1  /-
  2  Copyright (c) 2017 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Author: Johannes Hölzl
  5  
  6  Extended non-negative reals
  7  -/
  8  import topology.instances.nnreal data.real.ennreal
src         └───────────────────────┘ └───────────────┘
  9  noncomputable theory
 10  open classical set lattice filter metric
 11  open_locale classical
 12  open_locale topological_space
 13  variables {α : Type*} {β : Type*} {γ : Type*}
 14  
 15  open_locale ennreal
 16  
 17  namespace ennreal
 18  variables {a b c d : ennreal} {r p q : nnreal}
id                        └─────┘           └────┘
src                       └─────┘           └────┘
typ                       └─────┘           └────┘
doc                       └─────┘           └────┘
 19  variables {x y z : ennreal} {ε ε₁ ε₂ : ennreal} {s : set ennreal}
id                      └─────┘             └─────┘       └─┘ └─────┘
src                     └─────┘             └─────┘       └─┘ └─────┘
typ                     └─────┘             └─────┘       └─┘ └─────┘
doc                     └─────┘             └─────┘           └─────┘
 20  
 21  section topological_space
 22  open topological_space
 23  
 24  /-- Topology on `ennreal`.
 25  
 26  Note: this is different from the `emetric_space` topology. The `emetric_space` topology has
 27  `is_open {⊤}`, while this topology doesn't have singleton elements. -/
 28  instance : topological_space ennreal :=
id              └───────────────┘ └─────┘
src             └───────────────┘ └─────┘
typ             └───────────────┘ └─────┘
doc             └───────────────┘ └─────┘
 29  topological_space.generate_from {s | ∃a, s = {b | a < b} ∨ s = {b | b < a}}
id   └─────────────────────────────┘                      
src  └─────────────────────────────┘                              
typ  └─────────────────────────────┘                      
doc  └─────────────────────────────┘
 30  
 31  instance : order_topology ennreal := ⟨rfl⟩
id              └────────────┘ └─────┘     └─┘
src             └────────────┘ └─────┘     └─┘
typ             └────────────┘ └─────┘     └─┘
doc             └────────────┘ └─────┘
 32  
 33  instance : t2_space ennreal := by apply_instance -- short-circuit type class inference
id              └──────┘ └─────┘
src             └──────┘ └─────┘       └────────────────────────────────────────────────────
typ             └──────┘ └─────┘       └────────────────────────────────────────────────────
doc             └──────┘ └─────┘       └────────────────────────────────────────────────────
txt                                    └────────────────────────────────────────────────────
par                                    └────────────────────────────────────────────────────
pid                                                  └──────────────────────────────────────
st                                    └─────────────────────────────────────────────────────
 34  
src  
typ  
doc  
txt  
par  
pid  
st   
 35  instance : second_countable_topology ennreal :=
 36  ⟨⟨⋃q ≥ (0:ℚ), {{a : ennreal | a < nnreal.of_real q}, {a : ennreal | ↑(nnreal.of_real q) < a}},
 37    countable_bUnion (countable_encodable _) $ assume a ha, countable_insert (countable_singleton _),
 38    le_antisymm
 39      (le_generate_from $ by simp [or_imp_distrib, is_open_lt', is_open_gt'] {contextual := tt})
src                             └────┘              └┘           └┘           └┘ └────────────┘  
typ                             └────┘              └┘           └┘           └┘ └────────────┘  
doc                             └────┘              └┘           └┘           └┘ └────────────┘  
txt                             └────┘              └┘           └┘           └┘ └────────────┘  
par                             └────┘              └┘           └┘           └┘ └────────────┘  
pid                                               └┘           └┘            └────────────┘  
 40      (le_generate_from $ λ s h, begin
 41        rcases h with ⟨a, hs | hs⟩;
src        └─────┘ └────────────────┘
typ        └─────┘ └────────────────┘
doc        └─────┘ └────────────────┘
txt        └─────┘ └────────────────┘
par        └─────┘ └────────────────┘
pid               └────────────────┘
 42        [ rw show s = ⋃q∈{q:ℚ | 0 ≤ q ∧ a < nnreal.of_real q}, {b | ↑(nnreal.of_real q) < b},
src          └─┘       └┘ └┘ └───┘                      └──┘                 └┘  └──
typ          └─┘       └┘ └┘ └───┘                      └──┘                 └┘  └──
doc          └─┘       └┘ └┘ └───┘                      └──┘                 └┘  └──
txt          └─┘       └┘ └┘ └───┘                      └──┘                 └┘  └──
par          └─┘       └┘ └┘ └───┘                      └──┘                 └┘  └──
pid                   └┘ └┘ └───┘                      └──┘                 └┘  └──
 43             from set.ext (assume b, by simp [hs, @ennreal.lt_iff_exists_rat_btwn a b, and_assoc]),
src  ───────────────┘              └──┘  └────┘  └┘                                 └┘         
typ  ───────────────┘              └──┘  └────┘  └┘                                 └┘         
doc  ───────────────┘              └──┘  └────┘  └┘                                 └┘         
txt  ───────────────┘              └──┘  └────┘  └┘                                 └┘         
par  ───────────────┘              └──┘  └────┘  └┘                                 └┘         
pid  ───────────────┘              └──┘  └─────┘  └┘                                 └┘         └┘
 44          rw show s = ⋃q∈{q:ℚ | 0 ≤ q ∧ ↑(nnreal.of_real q) < a}, {b | b < ↑(nnreal.of_real q)},
src          └─┘       └┘ └┘ └───┘                    └┘    └──┘                   └───
typ          └─┘       └┘ └┘ └───┘                    └┘    └──┘                   └───
doc          └─┘       └┘ └┘ └───┘                    └┘    └──┘                   └───
txt          └─┘       └┘ └┘ └───┘                    └┘    └──┘                   └───
par          └─┘       └┘ └┘ └───┘                    └┘    └──┘                   └───
pid                   └┘ └┘ └───┘                    └┘    └──┘                   └───
 45             from set.ext (assume b, by simp [hs, @ennreal.lt_iff_exists_rat_btwn b a, and_comm, and_assoc])];
id                                                                         └───────┘    └──────┘  └───────┘
src  ───────────────┘              └──┘  └────┘  └┘                      └───────┘  └┘└──────┘└┘└───────┘
typ  ───────────────┘              └──┘  └────┘  └┘                      └───────┘└┘└──────┘└┘└───────┘
doc  ───────────────┘              └──┘  └────┘  └┘                                 └┘        └┘         
txt  ───────────────┘              └──┘  └────┘  └┘                                 └┘        └┘         
par  ───────────────┘              └──┘  └────┘  └┘                                 └┘        └┘         
pid  ───────────────┘              └──┘  └─────┘  └┘                                 └┘        └┘         └┘
st                                                                         └─────────────────────────────────┘└───
 46        { apply is_open_Union, intro q,
id                 └───────────┘
src          └────┘└───────────┘  └─────┘
typ          └────┘└───────────┘  └─────┘
doc          └────┘               └─────┘
txt          └────┘               └─────┘
par          └────┘               └─────┘
pid                                   └┘
st   ─────┘└───────────────────┘└───────┘└─
 47          apply is_open_Union, intro hq,
id                 └───────────┘
src          └────┘└───────────┘  └──────┘
typ          └────┘└───────────┘  └──────┘
doc          └────┘               └──────┘
txt          └────┘               └──────┘
par          └────┘               └──────┘
pid                                   └─┘
st   ──────────────────────────┘└────────┘└─
 48          exact generate_open.basic _ (mem_bUnion hq.1 $ by simp) }
id                 └─────────────────┘    └────────┘ └┘
src          └────┘└─────────────────┘└─┘ └────────┘  └─┘   └──┘└┘
typ          └────┘└─────────────────┘└─┘ └────────┘└┘└─┘   └──┘└┘
doc          └────┘                   └─┘             └─┘   └──┘└┘
txt          └────┘                   └─┘             └─┘   └──┘└┘
par          └────┘                   └─┘             └─┘   └──┘└┘
pid                                  └─┘             └─┘   └────┘
st   ────────────────────────────────────────────────────────┘└───┘└┘└─
 49      end)⟩⟩
st   ──────┘
 50  
 51  lemma embedding_coe : embedding (coe : nnreal → ennreal) :=
id                         └───────┘  └─┘   └────┘   └─────┘
src                        └───────┘  └─┘   └────┘   └─────┘
typ                        └───────┘  └─┘   └────┘   └─────┘
doc                        └───────┘        └────┘   └─────┘
 52  ⟨⟨begin
st     └─────
 53    refine le_antisymm _ _,
id            └─────────┘
src    └─────┘└─────────┘└──┘
typ    └─────┘└─────────┘└──┘
doc    └─────┘           └──┘
txt    └─────┘           └──┘
par    └─────┘           └──┘
pid                     └──┘
st   ───────────────────────┘└─
 54    { rw [order_topology.topology_eq_generate_intervals ennreal,
id           └───────────────────────────────────────────┘ └─────┘
src      └──┘└───────────────────────────────────────────┘└─────┘└─
typ      └──┘└───────────────────────────────────────────┘└─────┘└─
doc      └──┘                                             └─────┘└─
txt      └──┘                                                    └─
par      └──┘                                                    └─
pid        └┘                                                    └─
st   ───┘└───────────────────────────────────────────────────────┘└─
 55        ← coinduced_le_iff_le_induced],
id           └─────────────────────────┘
src  ───────┘└─────────────────────────┘
typ  ───────┘└─────────────────────────┘
doc  ───────┘                           
txt  ───────┘                           
par  ───────┘                           
pid  ───────┘                           
st   ──────────────────────────────────┘└──
 56      refine le_generate_from (assume s ha, _),
id              └──────────────┘
src      └─────┘└──────────────┘       └───────┘
typ      └─────┘└──────────────┘       └───────┘
doc      └─────┘                       └───────┘
txt      └─────┘                       └───────┘
par      └─────┘                       └───────┘
pid                                   └───────┘
st   ───────────────────────────────────────────┘└─
 57      rcases ha with ⟨a, rfl | rfl⟩,
id              └┘
src      └─────┘  └──────────────────┘
typ      └─────┘└┘└──────────────────┘
doc      └─────┘  └──────────────────┘
txt      └─────┘  └──────────────────┘
par      └─────┘  └──────────────────┘
pid              └──────────────────┘
st   ────────────────────────────────┘└─
 58      show is_open {b : nnreal | a < ↑b},
id            └─────┘     └────┘     
src      └───┘└─────┘└──┘└────┘└─┘  
typ      └───┘└─────┘└──┘└────┘└─┘ 
doc      └───┘└─────┘ └──┘└────┘└─┘    
txt      └───┘        └──┘      └─┘    
par      └───┘        └──┘      └─┘    
pid      └───┘        └──┘      └─┘    
st   ─────────────────────────────────────┘└─
 59      { cases a; simp [none_eq_top, some_eq_coe, is_open_lt'] },
id                       └─────────┘  └─────────┘  └─────────┘
src        └────┘   └────┘└─────────┘└┘└─────────┘└┘└─────────┘└┘
typ        └────┘  └────┘└─────────┘└┘└─────────┘└┘└─────────┘└┘
doc        └────┘   └────┘           └┘           └┘           └┘
txt        └────┘   └────┘           └┘           └┘           └┘
par        └────┘   └────┘           └┘           └┘           └┘
pid                               └┘           └┘           
st   ─────┘└────────────────────────────────────────────────────┘└┘
 60      show is_open {b : nnreal | ↑b < a},
id            └─────┘     └────┘        
src      └───┘└─────┘└──┘└────┘└─┘    
typ      └───┘└─────┘└──┘└────┘└─┘   
doc      └───┘└─────┘ └──┘└────┘└─┘    
txt      └───┘        └──┘      └─┘    
par      └───┘        └──┘      └─┘    
pid      └───┘        └──┘      └─┘    
st   ─────────────────────────────────────┘└─
 61      { cases a; simp [none_eq_top, some_eq_coe, is_open_gt', is_open_const] } },
id                       └─────────┘  └─────────┘  └─────────┘  └───────────┘
src        └────┘   └────┘└─────────┘└┘└─────────┘└┘└─────────┘└┘└───────────┘└┘
typ        └────┘  └────┘└─────────┘└┘└─────────┘└┘└─────────┘└┘└───────────┘└┘
doc        └────┘   └────┘           └┘           └┘           └┘             └┘
txt        └────┘   └────┘           └┘           └┘           └┘             └┘
par        └────┘   └────┘           └┘           └┘           └┘             └┘
pid                               └┘           └┘           └┘             
st   ──────────────────────────────────────────────────────────────────────────┘└──┘
 62    { rw [order_topology.topology_eq_generate_intervals nnreal],
id           └───────────────────────────────────────────┘ └────┘
src      └──┘└───────────────────────────────────────────┘└────┘
typ      └──┘└───────────────────────────────────────────┘└────┘
doc      └──┘                                             └────┘
txt      └──┘                                                   
par      └──┘                                                   
pid        └┘                                                   
st   ───────────────────────────────────────────────────────────┘└──
 63      refine le_generate_from (assume s ha, _),
id              └──────────────┘
src      └─────┘└──────────────┘       └───────┘
typ      └─────┘└──────────────┘       └───────┘
doc      └─────┘                       └───────┘
txt      └─────┘                       └───────┘
par      └─────┘                       └───────┘
pid                                   └───────┘
st   ───────────────────────────────────────────┘└─
 64      rcases ha with ⟨a, rfl | rfl⟩,
id              └┘
src      └─────┘  └──────────────────┘
typ      └─────┘└┘└──────────────────┘
doc      └─────┘  └──────────────────┘
txt      └─────┘  └──────────────────┘
par      └─────┘  └──────────────────┘
pid              └──────────────────┘
st   ────────────────────────────────┘└─
 65      exact ⟨Ioi a, is_open_Ioi, by simp [Ioi]⟩,
id              └─┘   └─────────┘           └─┘
src      └────┘ └─┘ └┘└─────────┘└┘  └────┘└─┘
typ      └────┘ └─┘└┘└─────────┘└┘  └────┘└─┘
doc      └────┘ └─┘ └┘           └┘  └────┘└─┘
txt      └────┘     └┘           └┘  └────┘   
par      └────┘     └┘           └┘  └────┘   
pid                └┘           └┘  └─────┘   └┘
st   ────────────────────────────────┘└─────────┘└─
 66      exact ⟨Iio a, is_open_Iio, by simp [Iio]⟩ }
id              └─┘   └─────────┘           └─┘
src      └────┘ └─┘ └┘└─────────┘└┘  └────┘└─┘└┘
typ      └────┘ └─┘└┘└─────────┘└┘  └────┘└─┘└┘
doc      └────┘ └─┘ └┘           └┘  └────┘└─┘└┘
txt      └────┘     └┘           └┘  └────┘   └┘
par      └────┘     └┘           └┘  └────┘   └┘
pid                └┘           └┘  └─────┘   └┘
st   ────────────────────────────────┘└─────────┘└┘└─
 67    end⟩,
st   ────┘
 68    assume a b, coe_eq_coe.1⟩
id               └────────┘
src                └────────┘
typ              └────────┘
 69  
 70  lemma is_open_ne_top : is_open {a : ennreal | a ≠ ⊤} :=
id                          └─────┘     └─────┘     
src                         └─────┘     └─────┘      
typ                         └─────┘     └─────┘     
doc                         └─────┘      └─────┘
 71  is_open_neg (is_closed_eq continuous_id continuous_const)
id   └─────────┘  └──────────┘ └───────────┘ └──────────────┘
src  └─────────┘  └──────────┘ └───────────┘ └──────────────┘
typ  └─────────┘  └──────────┘ └───────────┘ └──────────────┘
 72  
 73  lemma is_open_Ico_zero : is_open (Ico 0 b) := by { rw ennreal.Ico_eq_Iio, exact is_open_Iio}
id                            └─────┘  └─┘                └────────────────┘        └─────────┘
src                           └─────┘  └─┘              └─┘└────────────────┘  └────┘└─────────┘
typ                           └─────┘  └─┘             └─┘└────────────────┘  └────┘└─────────┘
doc                           └─────┘  └─┘              └─┘                    └────┘
txt                                                     └─┘                    └────┘
par                                                     └─┘                    └────┘
pid                                                                                
st                                                   └──────────────────────┘└─────────────────┘└┘
 74  
 75  lemma coe_range_mem_nhds : range (coe : nnreal → ennreal) ∈ 𝓝 (r : ennreal) :=
id                              └───┘  └─┘   └────┘   └─────┘        └─────┘
src                             └───┘  └─┘   └────┘   └─────┘         └─────┘
typ                             └───┘  └─┘   └────┘   └─────┘        └─────┘
doc                             └───┘        └────┘   └─────┘          └─────┘
 76  have {a : ennreal | a ≠ ⊤} = range (coe : nnreal → ennreal),
id            └─────┘        └───┘  └─┘   └────┘   └─────┘
src           └─────┘         └───┘  └─┘   └────┘   └─────┘
typ           └─────┘        └───┘  └─┘   └────┘   └─────┘
doc            └─────┘            └───┘        └────┘   └─────┘
 77    from set.ext $ assume a, by cases a; simp [none_eq_top, some_eq_coe],
id          └─────┘                             └─────────┘  └─────────┘
src         └─────┘                └────┘   └────┘└─────────┘└┘└─────────┘
typ         └─────┘               └────┘  └────┘└─────────┘└┘└─────────┘
doc                                └────┘   └────┘           └┘           
txt                                └────┘   └────┘           └┘           
par                                └────┘   └────┘           └┘           
pid                                                       └┘           
st                                └───────────────────────────────────────┘
 78  this ▸ mem_nhds_sets is_open_ne_top coe_ne_top
id   └──┘  └───────────┘ └────────────┘ └────────┘
src        └───────────┘ └────────────┘ └────────┘
typ  └──┘  └───────────┘ └────────────┘ └────────┘
 79  
 80  @[elim_cast] lemma tendsto_coe {f : filter α} {m : α → nnreal} {a : nnreal} :
id                                       └────┘           └────┘       └────┘
src                                      └────┘             └────┘       └────┘
typ                                      └────┘           └────┘       └────┘
doc    └───────┘                                            └────┘       └────┘
 81    tendsto (λa, (m a : ennreal)) f (𝓝 ↑a) ↔ tendsto m f (𝓝 a) :=
id     └─────┘          └─────┘         └─────┘     
src    └─────┘             └─────┘           └─────┘      
typ    └─────┘          └─────┘         └─────┘     
doc    └─────┘             └─────┘             └─────┘      
 82  embedding_coe.tendsto_nhds_iff.symm
id   └───────────┘└───────────────┘└───┘
src  └───────────┘└───────────────┘└───┘
typ  └───────────┘└───────────────┘└───┘
 83  
 84  lemma continuous_coe {α} [topological_space α] {f : α → nnreal} :
id                             └───────────────┘           └────┘
src                            └───────────────┘             └────┘
typ                            └───────────────┘           └────┘
doc                            └───────────────┘             └────┘
 85  continuous (λa, (f a : ennreal)) ↔ continuous f :=
id   └────────┘          └─────┘    └────────┘ 
src  └────────┘             └─────┘    └────────┘
typ  └────────┘          └─────┘    └────────┘ 
doc  └────────┘             └─────┘     └────────┘
 86  embedding_coe.continuous_iff.symm
id   └───────────┘└─────────────┘└───┘
src  └───────────┘└─────────────┘└───┘
typ  └───────────┘└─────────────┘└───┘
 87  
 88  lemma nhds_coe {r : nnreal} : 𝓝 (r : ennreal) = (𝓝 r).map coe :=
id                       └────┘         └─────┘      └─┘  └─┘
src                      └────┘          └─────┘       └─┘  └─┘
typ                      └────┘         └─────┘      └─┘  └─┘
doc                      └────┘          └─────┘        └─┘
 89  by rw [embedding_coe.induced, map_nhds_induced_eq coe_range_mem_nhds]
id                                 └─────────────────┘ └────────────────┘
src     └──┘                     └┘└─────────────────┘└────────────────┘└─
typ     └──┘└───────────────────┘└┘└─────────────────┘└────────────────┘└─
doc     └──┘                     └┘                                     └─
txt     └──┘                     └┘                                     └─
par     └──┘                     └┘                                     └─
pid       └┘                     └┘                                     
st     └────────────────────────┘└──────────────────────────────────────┘
 90  
src  
typ  
doc  
txt  
par  
pid  
st   
 91  lemma nhds_coe_coe {r p : nnreal} : 𝓝 ((r : ennreal), (p : ennreal)) =
id                             └────┘         └─────┘       └─────┘   
src                            └────┘          └─────┘        └─────┘   
typ                            └────┘         └─────┘       └─────┘   
doc                            └────┘           └─────┘        └─────┘
 92    (𝓝 (r, p)).map (λp:nnreal×nnreal, (p.1, p.2)) :=
id           └─┘      └────┘└────┘     
src            └─┘      └────┘└────┘       
typ          └─┘      └────┘└────┘     
doc             └─┘      └────┘ └────┘
 93  begin
st   └─────
 94    rw [(embedding_coe.prod_mk embedding_coe).map_nhds_eq],
id          └───────────────────┘ └───────────┘
src    └──┘ └───────────────────┘└───────────┘└────────────┘
typ    └──┘ └───────────────────┘└───────────┘└────────────┘
doc    └──┘                                   └────────────┘
txt    └──┘                                   └────────────┘
par    └──┘                                   └────────────┘
pid      └┘                                   └────────────┘
st   ─────────────────────────────────────────────────────┘└───
 95    rw [← prod_range_range_eq],
id           └─────────────────┘
src    └────┘└─────────────────┘
typ    └────┘└─────────────────┘
doc    └────┘                   
txt    └────┘                   
par    └────┘                   
pid      └──┘                   
st   ──────────────────────────┘└──
 96    exact prod_mem_nhds_sets coe_range_mem_nhds coe_range_mem_nhds
id           └────────────────┘                    └────────────────┘
src    └────┘└────────────────┘                  └────────────────┘
typ    └────┘└────────────────┘                  └────────────────┘
doc    └────┘                                                      
txt    └────┘                                                      
par    └────┘                                                      
pid                                                               
st   ────────────────────────────────────────────────────────────────┘
 97  end
st   └─┘
 98  
 99  lemma continuous_of_real : continuous ennreal.of_real :=
id                              └────────┘ └─────────────┘
src                             └────────┘ └─────────────┘
typ                             └────────┘ └─────────────┘
doc                             └────────┘ └─────────────┘
100  (continuous_coe.2 continuous_id).comp nnreal.continuous_of_real
id    └────────────┘  └───────────┘ └──┘  └───────────────────────┘
src   └────────────┘  └───────────┘ └──┘  └───────────────────────┘
typ   └────────────┘  └───────────┘ └──┘  └───────────────────────┘
101  
102  lemma tendsto_of_real {f : filter α} {m : α → ℝ} {a : ℝ} (h : tendsto m f (𝓝 a)) :
id                              └────┘                         └─────┘     
src                             └────┘                           └─────┘      
typ                             └────┘                         └─────┘     
doc                                                                └─────┘      
103    tendsto (λa, ennreal.of_real (m a)) f (𝓝 (ennreal.of_real a)) :=
id     └─────┘     └─────────────┘          └─────────────┘ 
src    └─────┘      └─────────────┘             └─────────────┘
typ    └─────┘     └─────────────┘          └─────────────┘ 
doc    └─────┘      └─────────────┘             └─────────────┘
104  tendsto.comp (continuous.tendsto continuous_of_real _) h
id   └──────────┘  └────────────────┘ └────────────────┘    
src  └──────────┘  └────────────────┘ └────────────────┘
typ  └──────────┘  └────────────────┘ └────────────────┘    
105  
106  lemma tendsto_to_nnreal {a : ennreal} : a ≠ ⊤ →
id                                └─────┘      
src                               └─────┘       
typ                               └─────┘      
doc                               └─────┘
107    tendsto (ennreal.to_nnreal) (𝓝 a) (𝓝 a.to_nnreal) :=
id     └─────┘  └───────────────┘        └────────┘
src    └─────┘  └───────────────┘          └────────┘
typ    └─────┘  └───────────────┘        └────────┘
doc    └─────┘  └───────────────┘          └────────┘
108  begin
st   └─────
109    cases a; simp [some_eq_coe, none_eq_top, nhds_coe, tendsto_map'_iff, (∘)],
id                   └─────────┘  └─────────┘  └──────┘  └──────────────┘  
src    └────┘   └────┘└─────────┘└┘└─────────┘└┘└──────┘└┘└──────────────┘└┘└─┘
typ    └────┘  └────┘└─────────┘└┘└─────────┘└┘└──────┘└┘└──────────────┘└┘└─┘
doc    └────┘   └────┘           └┘           └┘        └┘                └┘ └─┘
txt    └────┘   └────┘           └┘           └┘        └┘                └┘ └─┘
par    └────┘   └────┘           └┘           └┘        └┘                └┘ └─┘
pid                           └┘           └┘        └┘                └┘ └─┘
st   ──────────────────────────────────────────────────────────────────────────┘└─
110    exact tendsto_id
id           └────────┘
src    └────┘└────────┘
typ    └────┘└────────┘
doc    └────┘          
txt    └────┘          
par    └────┘          
pid                   
st   ──────────────────┘
111  end
st   └─┘
112  
113  lemma tendsto_to_real {a : ennreal} : a ≠ ⊤ → tendsto (ennreal.to_real) (𝓝 a) (𝓝 a.to_real) :=
id                              └─────┘         └─────┘  └─────────────┘        └──────┘
src                             └─────┘          └─────┘  └─────────────┘          └──────┘
typ                             └─────┘         └─────┘  └─────────────┘        └──────┘
doc                             └─────┘            └─────┘  └─────────────┘          └──────┘
114  λ ha, tendsto.comp ((@nnreal.tendsto_coe _ (𝓝 a.to_nnreal) id (a.to_nnreal)).2 tendsto_id)
id     └┘  └──────────┘    └────────────────┘     └────────┘  └┘  └────────┘    └────────┘
src        └──────────┘    └────────────────┘      └────────┘  └┘   └────────┘    └────────┘
typ    └┘  └──────────┘    └────────────────┘     └────────┘  └┘  └────────┘    └────────┘
doc                                                └────────┘       └────────┘
115    (tendsto_to_nnreal ha)
id      └───────────────┘ └┘
src     └───────────────┘
typ     └───────────────┘ └┘
116  
117  lemma tendsto_nhds_top {m : α → ennreal} {f : filter α}
id                                  └─────┘       └────┘ 
src                                  └─────┘       └────┘
typ                                 └─────┘       └────┘ 
doc                                  └─────┘
118    (h : ∀ n : ℕ, ∀ᶠ a in f, ↑n < m a) : tendsto m f (𝓝 ⊤) :=
id                  └┘  └┘         └─────┘     
src                 └┘   └┘             └─────┘       
typ                 └┘  └┘         └─────┘     
doc                  └┘   └┘               └─────┘      
119  tendsto_nhds_generate_from $ assume s hs,
id   └────────────────────────┘           └┘
src  └────────────────────────┘
typ  └────────────────────────┘           └┘
120  match s, hs with
id           └┘
typ          └┘
121  | _, ⟨none,   or.inl rfl⟩, hr := (lt_irrefl ⊤ hr).elim
id         └──┘    └────┘ └─┘   └┘     └───────┘     └──┘
src        └──┘    └────┘ └─┘          └───────┘     └──┘
typ        └──┘    └────┘ └─┘   └┘     └───────┘     └──┘
122  | _, ⟨some r, or.inl rfl⟩, hr :=
id         └──┘   └────┘ └─┘
src        └──┘    └────┘ └─┘
typ        └──┘   └────┘ └─┘
123    let ⟨n, hrn⟩ := exists_nat_gt r in
id     └─┘    └─┘     └───────────┘
src                    └───────────┘
typ    └─┘    └─┘     └───────────┘
124    mem_sets_of_superset (h n) $ assume a hnma, show ↑r < m a, from
id     └──────────────────┘                └──┘           
src    └──────────────────┘                               
typ    └──────────────────┘                └──┘           
125      lt_trans (show (r : ennreal) < n, from (coe_nat n) ▸ coe_lt_coe.2 hrn) hnma
id       └──────┘            └─────┘            └─────┘     └────────┘       └──┘
src      └──────┘            └─────┘            └─────┘     └────────┘
typ      └──────┘            └─────┘            └─────┘     └────────┘       └──┘
doc                          └─────┘
126  | _, ⟨a,      or.inr rfl⟩, hr := (not_top_lt $ show ⊤ < a, from hr).elim
id                └────┘ └─┘   └┘     └────────┘                     └──┘
src                └────┘ └─┘          └────────┘                     └──┘
typ               └────┘ └─┘   └┘     └────────┘                     └──┘
127  end
128  
129  lemma tendsto_nat_nhds_top : tendsto (λ n : ℕ, ↑n) at_top (𝓝 ∞) :=
id                                └─────┘            └────┘   
src                               └─────┘             └────┘   
typ                               └─────┘            └────┘   
doc                               └─────┘               └────┘   
130  tendsto_nhds_top $ λ n, mem_at_top_sets.2
id   └──────────────┘       └─────────────┘
src  └──────────────┘        └─────────────┘
typ  └──────────────┘       └─────────────┘
131    ⟨n+1, λ m hm, ennreal.coe_nat_lt_coe_nat.2 $ nat.lt_of_succ_le hm⟩
id            └┘  └────────────────────────┘    └───────────────┘ └┘
src                 └────────────────────────┘    └───────────────┘
typ           └┘  └────────────────────────┘    └───────────────┘ └┘
132  
133  lemma nhds_top : 𝓝 ∞ = ⨅a ≠ ∞, principal (Ioi a) :=
id                           └───────┘  └─┘ 
src                           └───────┘  └─┘
typ                          └───────┘  └─┘ 
doc                            └───────┘  └─┘
134  nhds_top_order.trans $ by simp [lt_top_iff_ne_top, Ioi]
id   └────────────┘└────┘            └───────────────┘  └─┘
src  └────────────┘└────┘      └────┘└───────────────┘└┘└─┘└─
typ  └────────────┘└────┘      └────┘└───────────────┘└┘└─┘└─
doc                            └────┘                 └┘└─┘└─
txt                            └────┘                 └┘   └─
par                            └────┘                 └┘   └─
pid                                                 └┘   
st                            └──────────────────────────────
135  
src  
typ  
doc  
txt  
par  
pid  
st   
136  lemma nhds_zero : 𝓝 (0 : ennreal) = ⨅a ≠ 0, principal (Iio a) :=
id                           └─────┘        └───────┘  └─┘ 
src                          └─────┘         └───────┘  └─┘
typ                          └─────┘        └───────┘  └─┘ 
doc                          └─────┘          └───────┘  └─┘
137  nhds_bot_order.trans $ by simp [bot_lt_iff_ne_bot, Iio]
id   └────────────┘└────┘            └───────────────┘  └─┘
src  └────────────┘└────┘      └────┘└───────────────┘└┘└─┘└─
typ  └────────────┘└────┘      └────┘└───────────────┘└┘└─┘└─
doc                            └────┘                 └┘└─┘└─
txt                            └────┘                 └┘   └─
par                            └────┘                 └┘   └─
pid                                                 └┘   
st                            └──────────────────────────────
138  
src  
typ  
doc  
txt  
par  
pid  
st   
139  -- using Icc because
src  ─────────────────────
typ  ─────────────────────
doc  ─────────────────────
txt  ─────────────────────
par  ─────────────────────
pid  ─────────────────────
st   ─────────────────────
140  -- • don't have 'Ioo (x - ε) (x + ε) ∈ 𝓝 x' unless x > 0
src  ─────────────────────────────────────────────────────────
typ  ─────────────────────────────────────────────────────────
doc  ─────────────────────────────────────────────────────────
txt  ─────────────────────────────────────────────────────────
par  ─────────────────────────────────────────────────────────
pid  ─────────────────────────────────────────────────────────
st   ─────────────────────────────────────────────────────────
141  -- • (x - y ≤ ε ↔ x ≤ ε + y) is true, while (x - y < ε ↔ x < ε + y) is not
src  ──────────────────────────────────────────────────────────────────────────┘
typ  ──────────────────────────────────────────────────────────────────────────┘
doc  ──────────────────────────────────────────────────────────────────────────┘
txt  ──────────────────────────────────────────────────────────────────────────┘
par  ──────────────────────────────────────────────────────────────────────────┘
pid  ──────────────────────────────────────────────────────────────────────────┘
st   ──────────────────────────────────────────────────────────────────────────┘
142  lemma Icc_mem_nhds : x ≠ ⊤ → ε > 0 → Icc (x - ε) (x + ε) ∈ 𝓝 x :=
id                                   └─┘             
src                                    └─┘                
typ                                  └─┘             
doc                                       └─┘                   
143  begin
st   └─────
144    assume xt ε0, rw mem_nhds_sets_iff,
id                      └───────────────┘
src    └──────────┘  └─┘└───────────────┘
typ    └──────────┘  └─┘└───────────────┘
doc    └──────────┘  └─┘
txt    └──────────┘  └─┘
par    └──────────┘  └─┘
pid    └──────────┘    
st   ─────────────┘└────────────────────┘└─
145    by_cases x0 : x = 0,
id                    
src    └───────┘  └─┘ └┘
typ    └───────┘  └─┘└┘
doc    └───────┘  └─┘  └┘
txt    └───────┘  └─┘  └┘
par    └───────┘  └─┘  └┘
pid              └─┘  
st   ────────────────────┘└─
146    { use Iio (x + ε),
id           └─┘    
src      └──┘└─┘   
typ      └──┘└─┘ 
doc      └──┘└─┘    
txt      └──┘       
par      └──┘       
pid                
st   ───┘└─────────────┘└─
147      have : Iio (x + ε) ⊆ Icc (x - ε) (x + ε), assume a, rw x0, simpa using le_of_lt,
id              └─┘          └─┘                            └┘              └──────┘
src      └─────┘└─┘    └┘└─┘   └┘      └──────┘  └─┘    └──────────┘└──────┘
typ      └─────┘└─┘    └┘└─┘   └┘    └──────┘  └─┘└┘  └──────────┘└──────┘
doc      └─────┘└─┘    └┘ └─┘    └┘      └──────┘  └─┘    └──────────┘
txt      └─────┘       └┘        └┘      └──────┘  └─┘    └──────────┘
par      └─────┘       └┘        └┘      └──────┘  └─┘    └──────────┘
pid      └───┘└┘       └┘        └┘      └──────┘             └────┘
st   ───────────────────────────────────────────┘└────────┘└─────┘└────────────────────┘└─
148      use this, exact ⟨is_open_Iio, mem_Iio_self_add xt ε0⟩ },
id           └──┘         └─────────┘  └──────────────┘ └┘ └┘
src      └──┘      └────┘ └─────────┘└┘└──────────────┘    └┘
typ      └──┘└──┘  └────┘ └─────────┘└┘└──────────────┘└┘└┘└┘
doc      └──┘      └────┘            └┘                    └┘
txt      └──┘      └────┘            └┘                    └┘
par      └──┘      └────┘            └┘                    └┘
pid                                └┘                    
st   ───────────┘└────────────────────────────────────────────┘└┘
149    { use Ioo (x - ε) (x + ε), use Ioo_subset_Icc_self,
id           └─┘                    └─────────────────┘
src      └──┘└─┘    └┘      └──┘└─────────────────┘
typ      └──┘└─┘    └┘    └──┘└─────────────────┘
doc      └──┘└─┘    └┘      └──┘
txt      └──┘       └┘      └──┘
par      └──┘       └┘      └──┘
pid                └┘         
st   ──────────────────────────┘└───────────────────────┘└─
150      exact ⟨is_open_Ioo, mem_Ioo_self_sub_add xt x0 ε0 ε0 ⟩ }
id              └─────────┘  └──────────────────┘ └┘ └┘    └┘
src      └────┘ └─────────┘└┘└──────────────────┘        └─┘
typ      └────┘ └─────────┘└┘└──────────────────┘└┘└┘  └┘└─┘
doc      └────┘            └┘                            └─┘
txt      └────┘            └┘                            └─┘
par      └────┘            └┘                            └─┘
pid                       └┘                            └┘
st   ──────────────────────────────────────────────────────────┘└─
151  end
st   ──┘
152  
153  lemma nhds_of_ne_top : x ≠ ⊤ → 𝓝 x = ⨅ε > 0, principal (Icc (x - ε) (x + ε)) :=
id                                       └───────┘  └─┘         
src                                         └───────┘  └─┘           
typ                                      └───────┘  └─┘         
doc                                            └───────┘  └─┘
154  begin
st   └─────
155    assume xt, refine le_antisymm _ _,
id                       └─────────┘
src    └───────┘  └─────┘└─────────┘└──┘
typ    └───────┘  └─────┘└─────────┘└──┘
doc    └───────┘  └─────┘           └──┘
txt    └───────┘  └─────┘           └──┘
par    └───────┘  └─────┘           └──┘
pid    └───────┘                   └──┘
st   ──────────┘└──────────────────────┘└─
156    -- first direction
st   ─────────────────────
157    simp only [le_infi_iff, le_principal_iff], assume ε ε0, exact Icc_mem_nhds xt ε0,
id                └─────────┘  └──────────────┘                      └──────────┘ └┘ └┘
src    └─────────┘└─────────┘└┘└──────────────┘  └─────────┘  └────┘└──────────┘  
typ    └─────────┘└─────────┘└┘└──────────────┘  └─────────┘  └────┘└──────────┘└┘└┘
doc    └─────────┘           └┘                  └─────────┘  └────┘              
txt    └─────────┘           └┘                  └─────────┘  └────┘              
par    └─────────┘           └┘                  └─────────┘  └────┘              
pid        └──┘└┘           └┘                  └─────────┘                     
st   ──────────────────────────────────────────┘└───────────┘└────────────────────────┘└─
158    -- second direction
st   ──────────────────────
159    rw nhds_generate_from, refine le_infi (assume s, le_infi $ assume hs, _),
id        └────────────────┘                            └─────┘
src    └─┘└────────────────┘  └─────┘              └──┘└─────┘       └─────┘
typ    └─┘└────────────────┘  └─────┘              └──┘└─────┘       └─────┘
doc    └─┘                    └─────┘              └──┘              └─────┘
txt    └─┘                    └─────┘              └──┘              └─────┘
par    └─┘                    └─────┘              └──┘              └─────┘
pid                                              └──┘              └─────┘
st   ──────────────────────┘└─────────────────────────────────────────────────┘└─
160    simp only [mem_set_of_eq] at hs, rcases hs with ⟨xs, ⟨a, ha⟩⟩,
id                └───────────┘                └┘
src    └─────────┘└───────────┘└─────┘  └─────┘  └─────────────────┘
typ    └─────────┘└───────────┘└─────┘  └─────┘└┘└─────────────────┘
doc    └─────────┘             └─────┘  └─────┘  └─────────────────┘
txt    └─────────┘             └─────┘  └─────┘  └─────────────────┘
par    └─────────┘             └─────┘  └─────┘  └─────────────────┘
pid        └──┘└┘             └───┘          └─────────────────┘
st   ────────────────────────────────┘└────────────────────────────┘└─
161    cases ha,
id           └┘
src    └────┘
typ    └────┘└┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────┘└─
162    { rw ha at *,
id          └┘
src      └─┘  └───┘
typ      └─┘└┘└───┘
doc      └─┘  └───┘
txt      └─┘  └───┘
par      └─┘  └───┘
pid          └───┘
st   ───┘└────────┘└─
163      rcases dense xs with ⟨b, ⟨ab, bx⟩⟩,
id              └───┘ └┘
src      └─────┘└───┘  └─────────────────┘
typ      └─────┘└───┘└┘└─────────────────┘
doc      └─────┘       └─────────────────┘
txt      └─────┘       └─────────────────┘
par      └─────┘       └─────────────────┘
pid                   └─────────────────┘
st   ─────────────────────────────────────┘└─
164      have xb_pos : x - b > 0 := zero_lt_sub_iff_lt.2 bx,
id                              └────────────────┘   └┘
src      └────────────┘  └────┘└────────────────┘└─┘
typ      └────────────┘└────┘└────────────────┘└─┘└┘
doc      └────────────┘    └────┘                  └─┘
txt      └────────────┘    └────┘                  └─┘
par      └────────────┘    └────┘                  └─┘
pid      └─────────┘└─┘    └───┘                  └─┘
st   ─────────────────────────────────────────────────────┘└─
165      have xxb : x - (x - b) = b := sub_sub_cancel (by rwa lt_top_iff_ne_top) (le_of_lt bx),
id                                  └────────────┘         └───────────────┘   └──────┘ └┘
src      └─────────┘      └┘ └──┘└────────────┘   └──┘└───────────────┘└┘ └──────┘  
typ      └─────────┘     └┘└──┘└────────────┘   └──┘└───────────────┘└┘ └──────┘└┘
doc      └─────────┘      └┘  └──┘                 └──┘                 └┘           
txt      └─────────┘      └┘  └──┘                 └──┘                 └┘           
par      └─────────┘      └┘  └──┘                 └──┘                 └┘           
pid      └──────┘└─┘      └┘  └──┘                 └───┘                 └┘           
st   ───────────────────────────────────────────────────┘└────────────────────┘└─────────────┘└─
166      refine infi_le_of_le (x - b) (infi_le_of_le xb_pos _),
id                                   └───────────┘ └────┘
src      └─────┘                 └┘ └───────────┘      └─┘
typ      └─────┘               └┘ └───────────┘└────┘└─┘
doc      └─────┘                 └┘                    └─┘
txt      └─────┘                 └┘                    └─┘
par      └─────┘                 └┘                    └─┘
pid                             └┘                    └─┘
st   ────────────────────────────────────────────────────────┘└─
167      simp only [mem_principal_sets, le_principal_iff],
id                  └────────────────┘  └──────────────┘
src      └─────────┘└────────────────┘└┘└──────────────┘
typ      └─────────┘└────────────────┘└┘└──────────────┘
doc      └─────────┘                  └┘                
txt      └─────────┘                  └┘                
par      └─────────┘                  └┘                
pid          └──┘└┘                  └┘                
st   ───────────────────────────────────────────────────┘└─
168      assume y, rintros ⟨h₁, h₂⟩, rw xxb at h₁, calc a < b : ab ... ≤ y : h₁ },
id                                      └─┘        └──┘       └┘          └┘
src      └──────┘  └──────────────┘  └─┘   └────┘  └──┘
typ      └──────┘  └──────────────┘  └─┘└─┘└────┘  └──┘       └┘          └┘
doc      └──────┘  └──────────────┘  └─┘   └────┘  └──┘
txt      └──────┘  └──────────────┘  └─┘   └────┘
par      └──────┘  └──────────────┘  └─┘   └────┘
pid      └──────┘         └───────┘       └────┘
st   ───────────┘└────────────────┘└────────────┘└────────────────────────────┘└─┘
169    { rw ha at *,
id          └┘
src      └─┘  └───┘
typ      └─┘└┘└───┘
doc      └─┘  └───┘
txt      └─┘  └───┘
par      └─┘  └───┘
pid          └───┘
st   ─────────────┘└─
170      rcases dense xs with ⟨b, ⟨xb, ba⟩⟩,
id              └───┘ └┘
src      └─────┘└───┘  └─────────────────┘
typ      └─────┘└───┘└┘└─────────────────┘
doc      └─────┘       └─────────────────┘
txt      └─────┘       └─────────────────┘
par      └─────┘       └─────────────────┘
pid                   └─────────────────┘
st   ─────────────────────────────────────┘└─
171      have bx_pos : b - x > 0 := zero_lt_sub_iff_lt.2 xb,
id                                └────────────────┘   └┘
src      └────────────┘    └────┘└────────────────┘└─┘
typ      └────────────┘  └────┘└────────────────┘└─┘└┘
doc      └────────────┘    └────┘                  └─┘
txt      └────────────┘    └────┘                  └─┘
par      └────────────┘    └────┘                  └─┘
pid      └─────────┘└─┘    └───┘                  └─┘
st   ─────────────────────────────────────────────────────┘└─
172      have xbx : x + (b - x) = b := add_sub_cancel_of_le (le_of_lt xb),
id                                  └──────────────────┘  └──────┘ └┘
src      └─────────┘     └┘  └──┘└──────────────────┘ └──────┘  
typ      └─────────┘    └┘ └──┘└──────────────────┘ └──────┘└┘
doc      └─────────┘      └┘  └──┘                               
txt      └─────────┘      └┘  └──┘                               
par      └─────────┘      └┘  └──┘                               
pid      └──────┘└─┘      └┘  └──┘                               
st   ───────────────────────────────────────────────────────────────────┘└─
173      refine infi_le_of_le (b - x) (infi_le_of_le bx_pos _),
id                                   └───────────┘ └────┘
src      └─────┘                 └┘ └───────────┘      └─┘
typ      └─────┘               └┘ └───────────┘└────┘└─┘
doc      └─────┘                 └┘                    └─┘
txt      └─────┘                 └┘                    └─┘
par      └─────┘                 └┘                    └─┘
pid                             └┘                    └─┘
st   ────────────────────────────────────────────────────────┘└─
174      simp only [mem_principal_sets, le_principal_iff],
id                  └────────────────┘  └──────────────┘
src      └─────────┘└────────────────┘└┘└──────────────┘
typ      └─────────┘└────────────────┘└┘└──────────────┘
doc      └─────────┘                  └┘                
txt      └─────────┘                  └┘                
par      └─────────┘                  └┘                
pid          └──┘└┘                  └┘                
st   ───────────────────────────────────────────────────┘└─
175      assume y, rintros ⟨h₁, h₂⟩, rw xbx at h₂, calc y ≤ b : h₂ ... < a : ba },
id                                      └─┘        └──┘       └┘          └┘
src      └──────┘  └──────────────┘  └─┘   └────┘  └──┘
typ      └──────┘  └──────────────┘  └─┘└─┘└────┘  └──┘       └┘          └┘
doc      └──────┘  └──────────────┘  └─┘   └────┘  └──┘
txt      └──────┘  └──────────────┘  └─┘   └────┘
par      └──────┘  └──────────────┘  └─┘   └────┘
pid      └──────┘         └───────┘       └────┘
st   ───────────┘└────────────────┘└────────────┘└────────────────────────────┘└───
176  end
st   ──┘
177  
178  /-- Characterization of neighborhoods for `ennreal` numbers. See also `tendsto_order`
179  for a version with strict inequalities. -/
180  protected theorem tendsto_nhds {f : filter α} {u : α → ennreal} {a : ennreal} (ha : a ≠ ⊤) :
id                                       └────┘           └─────┘       └─────┘          
src                                      └────┘             └─────┘       └─────┘           
typ                                      └────┘           └─────┘       └─────┘          
doc                                                         └─────┘       └─────┘
181    tendsto u f (𝓝 a) ↔ ∀ ε > 0, ∀ᶠ x in f, (u x) ∈ Icc (a - ε) (a + ε) :=
id     └─────┘                └┘  └┘       └─┘         
src    └─────┘                   └┘   └┘          └─┘           
typ    └─────┘                └┘  └┘       └─┘         
doc    └─────┘                     └┘   └┘           └─┘
182  by simp only [nhds_of_ne_top ha, tendsto_infi, tendsto_principal, mem_Icc]
id                 └────────────┘ └┘  └──────────┘  └───────────────┘  └─────┘
src     └─────────┘└────────────┘  └┘└──────────┘└┘└───────────────┘└┘└─────┘└─
typ     └─────────┘└────────────┘└┘└┘└──────────┘└┘└───────────────┘└┘└─────┘└─
doc     └─────────┘                └┘            └┘                 └┘       └─
txt     └─────────┘                └┘            └┘                 └┘       └─
par     └─────────┘                └┘            └┘                 └┘       └─
pid         └──┘└┘                └┘            └┘                 └┘       
st     └────────────────────────────────────────────────────────────────────────
183  
src  
typ  
doc  
txt  
par  
pid  
st   
184  protected lemma tendsto_at_top [nonempty β] [semilattice_sup β] {f : β → ennreal} {a : ennreal}
id                                   └──────┘    └─────────────┘           └─────┘       └─────┘
src                                  └──────┘     └─────────────┘             └─────┘       └─────┘
typ                                  └──────┘    └─────────────┘           └─────┘       └─────┘
doc                                               └─────────────┘             └─────┘       └─────┘
185    (ha : a ≠ ⊤) : tendsto f at_top (𝓝 a) ↔ ∀ε>0, ∃N, ∀n≥N, (f n) ∈ Icc (a - ε) (a + ε) :=
id                 └─────┘  └────┘                     └─┘         
src                 └─────┘   └────┘                           └─┘           
typ                └─────┘  └────┘                     └─┘         
doc                   └─────┘   └────┘                                └─┘
186  by simp only [ennreal.tendsto_nhds ha, mem_at_top_sets, mem_set_of_eq, filter.eventually]
id                 └──────────────────┘ └┘  └─────────────┘  └───────────┘  └───────────────┘
src     └─────────┘└──────────────────┘  └┘└─────────────┘└┘└───────────┘└┘└───────────────┘└─
typ     └─────────┘└──────────────────┘└┘└┘└─────────────┘└┘└───────────┘└┘└───────────────┘└─
doc     └─────────┘└──────────────────┘  └┘               └┘             └┘└───────────────┘└─
txt     └─────────┘                      └┘               └┘             └┘                 └─
par     └─────────┘                      └┘               └┘             └┘                 └─
pid         └──┘└┘                      └┘               └┘             └┘                 
st     └───────────────────────────────────────────────────────────────────────────────────────
187  
src  
typ  
doc  
txt  
par  
pid  
st   
188  lemma tendsto_coe_nnreal_nhds_top {α} {l : filter α} {f : α → nnreal} (h : tendsto f l at_top) :
id                                              └────┘           └────┘       └─────┘   └────┘
src                                             └────┘             └────┘       └─────┘     └────┘
typ                                             └────┘           └────┘       └─────┘   └────┘
doc                                                                └────┘       └─────┘     └────┘
189    tendsto (λa, (f a : ennreal)) l (𝓝 ∞) :=
id     └─────┘          └─────┘      
src    └─────┘             └─────┘       
typ    └─────┘          └─────┘      
doc    └─────┘             └─────┘       
190  tendsto_nhds_top $ assume n,
id   └──────────────┘          
src  └──────────────┘
typ  └──────────────┘          
191  have ∀ᶠ a in l, ↑(n+1) ≤ f a := h $ mem_at_top _,
id        └┘  └┘               └────────┘
src       └┘   └┘                    └────────┘
typ       └┘  └┘               └────────┘
doc       └┘   └┘  
192  mem_sets_of_superset this $ assume a (ha : ↑(n+1) ≤ f a),
id   └──────────────────┘ └──┘                       
src  └──────────────────┘                            
typ  └──────────────────┘ └──┘                       
193  begin
st   └─────
194    rw [← coe_nat],
id           └─────┘
src    └────┘└─────┘
typ    └────┘└─────┘
doc    └────┘       
txt    └────┘       
par    └────┘       
pid      └──┘       
st   ──────────────┘└──
195    dsimp,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
196    exact coe_lt_coe.2 (lt_of_lt_of_le (nat.cast_lt.2 (nat.lt_succ_self _)) ha)
id           └────────┘    └────────────┘  └─────────┘    └──────────────┘     └┘
src    └────┘└────────┘└─┘ └────────────┘ └─────────┘└─┘ └──────────────┘└───┘  └┘
typ    └────┘└────────┘└─┘ └────────────┘ └─────────┘└─┘ └──────────────┘└───┘└┘└┘
doc    └────┘          └─┘                           └─┘                 └───┘  └┘
txt    └────┘          └─┘                           └─┘                 └───┘  └┘
par    └────┘          └─┘                           └─┘                 └───┘  └┘
pid                   └─┘                           └─┘                 └───┘  
st   ─────────────────────────────────────────────────────────────────────────────┘
197  end
st   └─┘
198  
199  instance : topological_add_monoid ennreal :=
id              └────────────────────┘ └─────┘
src             └────────────────────┘ └─────┘
typ             └────────────────────┘ └─────┘
doc             └────────────────────┘ └─────┘
200  ⟨ continuous_iff_continuous_at.2 $
id     └──────────────────────────┘
src    └──────────────────────────┘
typ    └──────────────────────────┘
201    have hl : ∀a:ennreal, tendsto (λ (p : ennreal × ennreal), p.fst + p.snd) (𝓝 (⊤, a)) (𝓝 ⊤), from
id                  └─────┘  └─────┘         └─────┘  └─────┘   └──┘  └──┘           
src                 └─────┘  └─────┘         └─────┘  └─────┘    └──┘   └──┘            
typ                 └─────┘  └─────┘         └─────┘  └─────┘   └──┘  └──┘           
doc                 └─────┘  └─────┘         └─────┘   └─────┘                             
202      assume a, tendsto_nhds_top $ assume n,
id                └──────────────┘          
src                └──────────────┘
typ               └──────────────┘          
203      have set.prod {a | ↑n < a } univ ∈ 𝓝 ((⊤:ennreal), a), from
id            └──────┘         └──┘     └─────┘   
src           └──────┘            └──┘     └─────┘
typ           └──────┘         └──┘     └─────┘   
doc           └──────┘                           └─────┘
204        prod_mem_nhds_sets (lt_mem_nhds $ coe_nat n ▸ coe_lt_top) univ_mem_sets,
id         └────────────────┘  └─────────┘   └─────┘   └────────┘  └───────────┘
src        └────────────────┘  └─────────┘   └─────┘    └────────┘  └───────────┘
typ        └────────────────┘  └─────────┘   └─────┘   └────────┘  └───────────┘
205      show {a : ennreal × ennreal | ↑n < a.fst + a.snd} ∈ 𝓝 (⊤, a),
id                └─────┘  └─────┘     └──┘  └──┘      
src               └─────┘  └─────┘       └──┘   └──┘    
typ               └─────┘  └─────┘     └──┘  └──┘      
doc                └─────┘   └─────┘                         
206      begin filter_upwards [this] assume ⟨a₁, a₂⟩ ⟨h₁, h₂⟩, lt_of_lt_of_le h₁ (le_add_right $ le_refl _) end,
id                                                    └┘       └────────────┘     └──────────┘   └─────┘
src            └──────────────┘    └┘      └┘  └┘  └─┘  └┘  └─┘└────────────┘   └──────────┘ └─────┘└──┘
typ            └──────────────┘    └┘      └┘  └┘  └─┘└┘└┘  └─┘└────────────┘   └──────────┘ └─────┘└──┘
doc            └──────────────┘    └┘      └┘  └┘  └─┘  └┘  └─┘                                     └──┘
txt            └──────────────┘    └┘      └┘  └┘  └─┘  └┘  └─┘                                     └──┘
par            └──────────────┘    └┘      └┘  └┘  └─┘  └┘  └─┘                                     └──┘
pid                          └┘          └┘  └┘  └─┘  └┘  └─┘                                     └─┘
st       └─────────────────────────────────────────────────────────────────────────────────────────────────┘└─┘
207    begin
st     └─────
208      rintro ⟨a₁, a₂⟩,
src      └─────────────┘
typ      └─────────────┘
doc      └─────────────┘
txt      └─────────────┘
par      └─────────────┘
pid            └───────┘
st   ──────────────────┘└─
209      cases a₁, { simp [continuous_at, none_eq_top, hl a₂], },
id             └┘          └───────────┘  └─────────┘  └┘ └┘
src      └────┘      └────┘└───────────┘└┘└─────────┘└┘    
typ      └────┘└┘    └────┘└───────────┘└┘└─────────┘└┘└┘└┘
doc      └────┘      └────┘└───────────┘└┘           └┘    
txt      └────┘      └────┘             └┘           └┘    
par      └────┘      └────┘             └┘           └┘    
pid                                  └┘           └┘    
st   ───────────┘└──┘└──────────────────────────────────────┘└──┘
210      cases a₂, { simp [continuous_at, none_eq_top, some_eq_coe, nhds_swap (a₁ : ennreal) ⊤,
id             └┘          └───────────┘  └─────────┘  └─────────┘  └───────┘  └┘   └─────┘  
src      └────┘      └────┘└───────────┘└┘└─────────┘└┘└─────────┘└┘└───────┘   └─┘└─────┘└┘└─
typ      └────┘└┘    └────┘└───────────┘└┘└─────────┘└┘└─────────┘└┘└───────┘ └┘└─┘└─────┘└┘└─
doc      └────┘      └────┘└───────────┘└┘           └┘           └┘            └─┘└─────┘└┘ └─
txt      └────┘      └────┘             └┘           └┘           └┘            └─┘       └┘ └─
par      └────┘      └────┘             └┘           └┘           └┘            └─┘       └┘ └─
pid                                  └┘           └┘           └┘            └─┘       └┘ └─
st   ───────────┘└──┘└──────────────────────────────────────────────────────────────────────────
211                        tendsto_map'_iff, (∘), hl ↑a₁] },
id                         └──────────────┘      └┘ └┘
src  ─────────────────────┘└──────────────┘└┘└──┘    └┘
typ  ─────────────────────┘└──────────────┘└┘└──┘└┘└┘└┘
doc  ─────────────────────┘                └┘ └──┘     └┘
txt  ─────────────────────┘                └┘ └──┘     └┘
par  ─────────────────────┘                └┘ └──┘     └┘
pid  ─────────────────────┘                └┘ └──┘     
st   ────────────────────────────────────────────────────┘└┘
212      simp [continuous_at, some_eq_coe, nhds_coe_coe, tendsto_map'_iff, (∘)],
id             └───────────┘  └─────────┘  └──────────┘  └──────────────┘  
src      └────┘└───────────┘└┘└─────────┘└┘└──────────┘└┘└──────────────┘└┘└─┘
typ      └────┘└───────────┘└┘└─────────┘└┘└──────────┘└┘└──────────────┘└┘└─┘
doc      └────┘└───────────┘└┘           └┘            └┘                └┘ └─┘
txt      └────┘             └┘           └┘            └┘                └┘ └─┘
par      └────┘             └┘           └┘            └┘                └┘ └─┘
pid                       └┘           └┘            └┘                └┘ └─┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
213      simp only [coe_add.symm, tendsto_coe, tendsto_add]
id                                └─────────┘  └─────────┘
src      └─────────┘            └┘└─────────┘└┘└─────────┘└─
typ      └─────────┘└──────────┘└┘└─────────┘└┘└─────────┘└─
doc      └─────────┘            └┘           └┘           └─
txt      └─────────┘            └┘           └┘           └─
par      └─────────┘            └┘           └┘           └─
pid          └──┘└┘            └┘           └┘           
st   ───────────────────────────────────────────────────────
214    end ⟩
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
215  
216  protected lemma tendsto_mul (ha : a ≠ 0 ∨ b ≠ ⊤) (hb : b ≠ 0 ∨ a ≠ ⊤) :
id                                                           
src                                                              
typ                                                          
217    tendsto (λp:ennreal×ennreal, p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b)) :=
id     └─────┘     └─────┘└─────┘                    
src    └─────┘     └─────┘└─────┘                        
typ    └─────┘     └─────┘└─────┘                    
doc    └─────┘     └─────┘ └─────┘                        
218  have ht : ∀b:ennreal, b ≠ 0 → tendsto (λp:ennreal×ennreal, p.1 * p.2) (𝓝 ((⊤:ennreal), b)) (𝓝 ⊤),
id                └─────┘        └─────┘     └─────┘└─────┘            └─────┘        
src               └─────┘         └─────┘     └─────┘└─────┘              └─────┘         
typ               └─────┘        └─────┘     └─────┘└─────┘            └─────┘        
doc               └─────┘          └─────┘     └─────┘ └─────┘                   └─────┘        
219  begin
st   └─────
220    refine assume b hb, tendsto_nhds_top $ assume n, _,
id                         └──────────────┘
src    └─────┘      └─────┘└──────────────┘       └───┘
typ    └─────┘      └─────┘└──────────────┘       └───┘
doc    └─────┘      └─────┘                       └───┘
txt    └─────┘      └─────┘                       └───┘
par    └─────┘      └─────┘                       └───┘
pid                └─────┘                       └───┘
st   ───────────────────────────────────────────────────┘└─
221    rcases dense (zero_lt_iff_ne_zero.2 hb) with ⟨ε', hε', hεb'⟩,
id            └───┘  └─────────────────┘   └┘
src    └─────┘└───┘ └─────────────────┘└─┘  └────────────────────┘
typ    └─────┘└───┘ └─────────────────┘└─┘└┘└────────────────────┘
doc    └─────┘                         └─┘  └────────────────────┘
txt    └─────┘                         └─┘  └────────────────────┘
par    └─────┘                         └─┘  └────────────────────┘
pid                                   └─┘  └────────────────────┘
st   ─────────────────────────────────────────────────────────────┘└─
222    rcases ennreal.lt_iff_exists_coe.1 hεb' with ⟨ε, rfl, h⟩,
id            └───────────────────────┘   └──┘
src    └─────┘└───────────────────────┘└─┘    └───────────────┘
typ    └─────┘└───────────────────────┘└─┘└──┘└───────────────┘
doc    └─────┘                         └─┘    └───────────────┘
txt    └─────┘                         └─┘    └───────────────┘
par    └─────┘                         └─┘    └───────────────┘
pid                                   └─┘    └───────────────┘
st   ─────────────────────────────────────────────────────────┘└─
223    rcases exists_nat_gt (↑n / ε) with ⟨m, hm⟩,
id            └───────────┘    
src    └─────┘└───────────┘   └────────────┘
typ    └─────┘└───────────┘ └────────────┘
doc    └─────┘                  └────────────┘
txt    └─────┘                  └────────────┘
par    └─────┘                  └────────────┘
pid                            └────────────┘
st   ───────────────────────────────────────────┘└─
224    have hε : ε > 0, from coe_lt_coe.1 hε',
id                         └────────┘   └─┘
src    └────────┘ └┘  └───┘└────────┘└─┘
typ    └────────┘└┘  └───┘└────────┘└─┘└─┘
doc    └────────┘  └┘  └───┘          └─┘
txt    └────────┘  └┘  └───┘          └─┘
par    └────────┘  └┘  └───┘          └─┘
pid    └─────┘└─┘    └───┘          └─┘
st   ────────────────┘└─────────────────────┘└─
225    refine mem_sets_of_superset (prod_mem_nhds_sets (lt_mem_nhds $ @coe_lt_top m) (lt_mem_nhds $ h)) _,
id            └──────────────────┘  └────────────────┘                 └────────┘    └─────────┘   
src    └─────┘└──────────────────┘ └────────────────┘              └────────┘ └┘ └─────────┘  └──┘
typ    └─────┘└──────────────────┘ └────────────────┘              └────────┘└┘ └─────────┘ └──┘
doc    └─────┘                                                                └┘              └──┘
txt    └─────┘                                                                └┘              └──┘
par    └─────┘                                                                └┘              └──┘
pid                                                                          └┘              └──┘
st   ───────────────────────────────────────────────────────────────────────────────────────────────────┘└─
226    rintros ⟨a₁, a₂⟩ ⟨h₁, h₂⟩,
src    └───────────────────────┘
typ    └───────────────────────┘
doc    └───────────────────────┘
txt    └───────────────────────┘
par    └───────────────────────┘
pid           └────────────────┘
st   ──────────────────────────┘└─
227    dsimp at h₁ h₂ ⊢,
src    └──────────────┘
typ    └──────────────┘
doc    └──────────────┘
txt    └──────────────┘
par    └──────────────┘
pid         └────────┘
st   ─────────────────┘└─
228    calc (n:ennreal) = ↑(((n:nnreal) / ε) * ε) :
id     └──┘    └─────┘         └────┘         
src    └──┘    └─────┘          └────┘
typ    └──┘    └─────┘         └────┘         
doc    └──┘    └─────┘          └────┘
st   ───────────────────────────────────────────────
229      begin
st   ───┘└─────
230        simp [nnreal.div_def],
id               └────────────┘
src        └────┘└────────────┘
typ        └────┘└────────────┘
doc        └────┘              
txt        └────┘              
par        └────┘              
pid                          
st   ──────────────────────────┘└─
231        rw [mul_assoc, ← coe_mul, nnreal.inv_mul_cancel, coe_one, ← coe_nat, mul_one],
id             └───────┘    └─────┘  └───────────────────┘  └─────┘    └─────┘  └─────┘
src        └──┘└───────┘└──┘└─────┘└┘└───────────────────┘└┘└─────┘└──┘└─────┘└┘└─────┘
typ        └──┘└───────┘└──┘└─────┘└┘└───────────────────┘└┘└─────┘└──┘└─────┘└┘└─────┘
doc        └──┘         └──┘       └┘                     └┘       └──┘       └┘       
txt        └──┘         └──┘       └┘                     └┘       └──┘       └┘       
par        └──┘         └──┘       └┘                     └┘       └──┘       └┘       
pid          └┘         └──┘       └┘                     └┘       └──┘       └┘       
st   ──────────────────┘└─────────┘└─────────────────────┘└───────┘└─────────┘└───────┘└──
232        exact zero_lt_iff_ne_zero.1 hε
id               └─────────────────┘   └┘
src        └────┘└─────────────────┘└─┘  
typ        └────┘└─────────────────┘└─┘└┘
doc        └────┘                   └─┘  
txt        └────┘                   └─┘  
par        └────┘                   └─┘  
pid                                └─┘  
st   ─────────────────────────────────────
233      end
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
234      ... < (↑m * ε : nnreal) : coe_lt_coe.2 $ mul_lt_mul hm (le_refl _) hε (nat.cast_nonneg _)
id                               └────────┘    └────────┘ └┘  └─────┘    └┘  └─────────────┘
src                               └────────┘    └────────┘     └─────┘        └─────────────┘
typ                              └────────┘    └────────┘ └┘  └─────┘    └┘  └─────────────┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────
235      ... ≤ a₁ * a₂ : by rw [coe_mul]; exact canonically_ordered_semiring.mul_le_mul
id             └┘   └┘          └─────┘         └─────────────────────────────────────┘
src                         └──┘└─────┘  └────┘└─────────────────────────────────────┘
typ            └┘   └┘      └──┘└─────┘  └────┘└─────────────────────────────────────┘
doc                         └──┘         └────┘                                       
txt                         └──┘         └────┘                                       
par                         └──┘         └────┘                                       
pid                           └┘                                                     
st   ─────────────────────┘└──────────┘└───────────────────────────────────────────────
236        (le_of_lt h₁)
id                   └┘
src  ─────┘           └─
typ  ─────┘         └┘└─
doc  ─────┘           └─
txt  ─────┘           └─
par  ─────┘           └─
pid  ─────┘           └─
st   ────────────────────
237        (le_of_lt h₂)
id          └──────┘ └┘
src  ─────┘ └──────┘  └┘
typ  ─────┘ └──────┘└┘└┘
doc  ─────┘           └┘
txt  ─────┘           └┘
par  ─────┘           └┘
pid  ─────┘           
st   ───────────────────┘
238  end,
st   └─┘
239  begin
st   └─────
240    cases a, {simp [none_eq_top] at hb, simp [none_eq_top, ht b hb, top_mul, hb] },
id                    └─────────┘               └─────────┘  └┘  └┘  └─────┘  └┘
src    └────┘    └────┘└─────────┘└─────┘  └────┘└─────────┘└┘     └┘└─────┘└┘  └┘
typ    └────┘   └────┘└─────────┘└─────┘  └────┘└─────────┘└┘└┘└┘└┘└─────┘└┘└┘└┘
doc    └────┘    └────┘           └─────┘  └────┘           └┘     └┘       └┘  └┘
txt    └────┘    └────┘           └─────┘  └────┘           └┘     └┘       └┘  └┘
par    └────┘    └────┘           └─────┘  └────┘           └┘     └┘       └┘  └┘
pid                            └───┘                 └┘     └┘       └┘  
st   ────────┘└─────────────────────────┘└─────────────────────────────────────────┘└┘
241    cases b, {
id           
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ────────┘└──┘
242      simp [none_eq_top] at ha,
id             └─────────┘
src      └────┘└─────────┘└─────┘
typ      └────┘└─────────┘└─────┘
doc      └────┘           └─────┘
txt      └────┘           └─────┘
par      └────┘           └─────┘
pid                     └───┘
st   └──────────────────────────┘└─
243      have ha' : a ≠ 0, from mt coe_eq_coe.2 ha,
id                            └┘ └────────┘   └┘
src      └─────────┘ └┘  └───┘└┘└────────┘└─┘
typ      └─────────┘└┘  └───┘└┘└────────┘└─┘└┘
doc      └─────────┘  └┘  └───┘            └─┘
txt      └─────────┘  └┘  └───┘            └─┘
par      └─────────┘  └┘  └───┘            └─┘
pid      └──────┘└─┘    └───┘            └─┘
st   ───────────────────┘└───────────────────────┘└─
244      simp [*, nhds_swap (a : ennreal) ⊤, none_eq_top, some_eq_coe, top_mul, tendsto_map'_iff, (∘), mul_comm] },
id                └───────┘     └─────┘    └─────────┘  └─────────┘  └─────┘  └──────────────┘      └──────┘
src      └───────┘└───────┘  └─┘└─────┘└┘└┘└─────────┘└┘└─────────┘└┘└─────┘└┘└──────────────┘└┘└──┘└──────┘└┘
typ      └───────┘└───────┘ └─┘└─────┘└┘└┘└─────────┘└┘└─────────┘└┘└─────┘└┘└──────────────┘└┘└──┘└──────┘└┘
doc      └───────┘           └─┘└─────┘└┘ └┘           └┘           └┘       └┘                └┘ └──┘        └┘
txt      └───────┘           └─┘       └┘ └┘           └┘           └┘       └┘                └┘ └──┘        └┘
par      └───────┘           └─┘       └┘ └┘           └┘           └┘       └┘                └┘ └──┘        └┘
pid          └──┘           └─┘       └┘ └┘           └┘           └┘       └┘                └┘ └──┘        
st   ───────────────────────────────────────────────────────────────────────────────────────────────────────────┘└┘
245    simp [some_eq_coe, nhds_coe_coe, tendsto_map'_iff, (∘)],
id           └─────────┘  └──────────┘  └──────────────┘  
src    └────┘└─────────┘└┘└──────────┘└┘└──────────────┘└┘└─┘
typ    └────┘└─────────┘└┘└──────────┘└┘└──────────────┘└┘└─┘
doc    └────┘           └┘            └┘                └┘ └─┘
txt    └────┘           └┘            └┘                └┘ └─┘
par    └────┘           └┘            └┘                └┘ └─┘
pid                   └┘            └┘                └┘ └─┘
st   ────────────────────────────────────────────────────────┘└─
246    simp only [coe_mul.symm, tendsto_coe, tendsto_mul]
id                              └─────────┘  └─────────┘
src    └─────────┘            └┘└─────────┘└┘└─────────┘└┘
typ    └─────────┘└──────────┘└┘└─────────┘└┘└─────────┘└┘
doc    └─────────┘            └┘           └┘           └┘
txt    └─────────┘            └┘           └┘           └┘
par    └─────────┘            └┘           └┘           └┘
pid        └──┘└┘            └┘           └┘           
st   ────────────────────────────────────────────────────┘
247  end
st   └─┘
248  
249  protected lemma tendsto.mul {f : filter α} {ma : α → ennreal} {mb : α → ennreal} {a b : ennreal}
id                                    └────┘            └─────┘           └─────┘         └─────┘
src                                   └────┘              └─────┘            └─────┘         └─────┘
typ                                   └────┘            └─────┘           └─────┘         └─────┘
doc                                                       └─────┘            └─────┘         └─────┘
250    (hma : tendsto ma f (𝓝 a)) (ha : a ≠ 0 ∨ b ≠ ⊤) (hmb : tendsto mb f (𝓝 b)) (hb : b ≠ 0 ∨ a ≠ ⊤) :
id            └─────┘ └┘                             └─────┘ └┘                    
src           └─────┘                                    └─────┘                           
typ           └─────┘ └┘                             └─────┘ └┘                    
doc           └─────┘                                        └─────┘       
251    tendsto (λa, ma a * mb a) f (𝓝 (a * b)) :=
id     └─────┘     └┘   └┘         
src    └─────┘                         
typ    └─────┘     └┘   └┘         
doc    └─────┘                      
252  show tendsto ((λp:ennreal×ennreal, p.1 * p.2) ∘ (λa, (ma a, mb a))) f (𝓝 (a * b)), from
id        └─────┘      └─────┘└─────┘             └┘   └┘           
src       └─────┘      └─────┘└─────┘                                     
typ       └─────┘      └─────┘└─────┘             └┘   └┘           
doc       └─────┘      └─────┘ └─────┘                                      
253  tendsto.comp (ennreal.tendsto_mul ha hb) (tendsto_prod_mk_nhds hma hmb)
id   └──────────┘  └─────────────────┘ └┘ └┘   └──────────────────┘ └─┘ └─┘
src  └──────────┘  └─────────────────┘         └──────────────────┘
typ  └──────────┘  └─────────────────┘ └┘ └┘   └──────────────────┘ └─┘ └─┘
254  
255  protected lemma tendsto.const_mul {f : filter α} {m : α → ennreal} {a b : ennreal}
id                                          └────┘           └─────┘         └─────┘
src                                         └────┘             └─────┘         └─────┘
typ                                         └────┘           └─────┘         └─────┘
doc                                                            └─────┘         └─────┘
256    (hm : tendsto m f (𝓝 b)) (hb : b ≠ 0 ∨ a ≠ ⊤) : tendsto (λb, a * m b) f (𝓝 (a * b)) :=
id           └─────┘                         └─────┘                
src          └─────┘                              └─────┘                     
typ          └─────┘                         └─────┘                
doc          └─────┘                                  └─────┘                  
257  by_cases
id   └──────┘
src  └──────┘
typ  └──────┘
258    (assume : a = 0, by simp [this, tendsto_const_nhds])
id                             └──┘  └────────────────┘
src                       └────┘    └┘└────────────────┘
typ                      └────┘└──┘└┘└────────────────┘
doc                        └────┘    └┘                  
txt                        └────┘    └┘                  
par                        └────┘    └┘                  
pid                                └┘                  
st                        └──────────────────────────────┘
259    (assume ha : a ≠ 0, ennreal.tendsto.mul tendsto_const_nhds (or.inl ha) hm hb)
id                       └─────────────────┘ └────────────────┘  └────┘ └┘  └┘ └┘
src                       └─────────────────┘ └────────────────┘  └────┘
typ                      └─────────────────┘ └────────────────┘  └────┘ └┘  └┘ └┘
260  
261  protected lemma tendsto.mul_const {f : filter α} {m : α → ennreal} {a b : ennreal}
id                                          └────┘           └─────┘         └─────┘
src                                         └────┘             └─────┘         └─────┘
typ                                         └────┘           └─────┘         └─────┘
doc                                                            └─────┘         └─────┘
262    (hm : tendsto m f (𝓝 a)) (ha : a ≠ 0 ∨ b ≠ ⊤) : tendsto (λx, m x * b) f (𝓝 (a * b)) :=
id           └─────┘                         └─────┘                
src          └─────┘                              └─────┘                     
typ          └─────┘                         └─────┘                
doc          └─────┘                                  └─────┘                  
263  by simpa only [mul_comm] using ennreal.tendsto.const_mul hm ha
id                  └──────┘        └───────────────────────┘ └┘ └┘
src     └──────────┘└──────┘└──────┘└───────────────────────┘    
typ     └──────────┘└──────┘└──────┘└───────────────────────┘└┘└┘
doc     └──────────┘        └──────┘                             
txt     └──────────┘        └──────┘                             
par     └──────────┘        └──────┘                             
pid          └──┘└┘        └────┘                             
st     └────────────────────────────────────────────────────────────
264  
src  
typ  
doc  
txt  
par  
pid  
st   
265  protected lemma continuous_const_mul {a : ennreal} (ha : a < ⊤) : continuous ((*) a) :=
id                                             └─────┘              └────────┘     
src                                            └─────┘               └────────┘  
typ                                            └─────┘              └────────┘     
doc                                            └─────┘                 └────────┘
266  continuous_iff_continuous_at.2 $ λ x, tendsto.const_mul tendsto_id $ or.inr $ ne_of_lt ha
id   └──────────────────────────┘        └───────────────┘ └────────┘   └────┘   └──────┘ └┘
src  └──────────────────────────┘         └───────────────┘ └────────┘   └────┘   └──────┘
typ  └──────────────────────────┘        └───────────────┘ └────────┘   └────┘   └──────┘ └┘
267  
268  protected lemma continuous_mul_const {a : ennreal} (ha : a < ⊤) : continuous (λ x, x * a) :=
id                                             └─────┘              └────────┘        
src                                            └─────┘               └────────┘         
typ                                            └─────┘              └────────┘        
doc                                            └─────┘                 └────────┘
269  by simpa only [mul_comm] using ennreal.continuous_const_mul ha
id                  └──────┘        └──────────────────────────┘ └┘
src     └──────────┘└──────┘└──────┘└──────────────────────────┘  
typ     └──────────┘└──────┘└──────┘└──────────────────────────┘└┘
doc     └──────────┘        └──────┘                              
txt     └──────────┘        └──────┘                              
par     └──────────┘        └──────┘                              
pid          └──┘└┘        └────┘                              
st     └────────────────────────────────────────────────────────────
270  
src  
typ  
doc  
txt  
par  
pid  
st   
271  protected lemma continuous_inv : continuous (has_inv.inv : ennreal → ennreal) :=
id                                    └────────┘  └─────────┘   └─────┘   └─────┘
src                                   └────────┘  └─────────┘   └─────┘   └─────┘
typ                                   └────────┘  └─────────┘   └─────┘   └─────┘
doc                                   └────────┘                └─────┘   └─────┘
272  continuous_iff_continuous_at.2 $ λ a, tendsto_order.2
id   └──────────────────────────┘        └───────────┘
src  └──────────────────────────┘         └───────────┘
typ  └──────────────────────────┘        └───────────┘
273  ⟨begin
st    └─────
274    assume b hb,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
275    simp only [@ennreal.lt_inv_iff_lt_inv b],
id                 └───────────────────────┘ 
src    └─────────┘ └───────────────────────┘ 
typ    └─────────┘ └───────────────────────┘
doc    └─────────┘                           
txt    └─────────┘                           
par    └─────────┘                           
pid        └──┘└┘                           
st   ─────────────────────────────────────────┘└─
276    exact gt_mem_nhds (ennreal.lt_inv_iff_lt_inv.1 hb),
id           └─────────┘  └───────────────────────┘   └┘
src    └────┘└─────────┘ └───────────────────────┘└─┘  
typ    └────┘└─────────┘ └───────────────────────┘└─┘└┘
doc    └────┘                                     └─┘  
txt    └────┘                                     └─┘  
par    └────┘                                     └─┘  
pid                                              └─┘  
st   ───────────────────────────────────────────────────┘└─
277  end,
st   ──┘
278  begin
st   └─────
279    assume b hb,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
280    simp only [gt_iff_lt, @ennreal.inv_lt_iff_inv_lt _ b],
id                └───────┘   └───────────────────────┘   
src    └─────────┘└───────┘└┘ └───────────────────────┘└─┘ 
typ    └─────────┘└───────┘└┘ └───────────────────────┘└─┘
doc    └─────────┘         └┘                          └─┘ 
txt    └─────────┘         └┘                          └─┘ 
par    └─────────┘         └┘                          └─┘ 
pid        └──┘└┘         └┘                          └─┘ 
st   ──────────────────────────────────────────────────────┘└─
281    exact lt_mem_nhds (ennreal.inv_lt_iff_inv_lt.1 hb)
id           └─────────┘  └───────────────────────┘   └┘
src    └────┘└─────────┘ └───────────────────────┘└─┘  └┘
typ    └────┘└─────────┘ └───────────────────────┘└─┘└┘└┘
doc    └────┘                                     └─┘  └┘
txt    └────┘                                     └─┘  └┘
par    └────┘                                     └─┘  └┘
pid                                              └─┘  
st   ────────────────────────────────────────────────────┘
282  end⟩
st   └─┘
283  
284  @[simp] protected lemma tendsto_inv_iff {f : filter α} {m : α → ennreal} {a : ennreal} :
id                                                └────┘           └─────┘       └─────┘
src                                               └────┘             └─────┘       └─────┘
typ                                               └────┘           └─────┘       └─────┘
doc    └──┘                                                          └─────┘       └─────┘
285    tendsto (λ x, (m x)⁻¹) f (𝓝 a⁻¹) ↔ tendsto m f (𝓝 a) :=
id     └─────┘         └┘     └┘   └─────┘     
src    └─────┘            └┘       └┘   └─────┘      
typ    └─────┘         └┘     └┘   └─────┘     
doc    └─────┘                           └─────┘      
286  ⟨λ h, by simpa only [function.comp, ennreal.inv_inv]
id                       └───────────┘  └─────────────┘
src           └──────────┘└───────────┘└┘└─────────────┘└─
typ          └──────────┘└───────────┘└┘└─────────────┘└─
doc           └──────────┘             └┘               └─
txt           └──────────┘             └┘               └─
par           └──────────┘             └┘               └─
pid                └──┘└┘             └┘               
st           └────────────────────────────────────────────
287    using (ennreal.continuous_inv.tendsto a⁻¹).comp h,
id            └────────────────────────────┘ └┘       
src  ───────┘ └────────────────────────────┘ └┘└─────┘
typ  ───────┘ └────────────────────────────┘└┘└─────┘
doc  ───────┘                                  └─────┘
txt  ───────┘                                  └─────┘
par  ───────┘                                  └─────┘
pid  ─┘└────┘                                  └─────┘
st   ──────────────────────────────────────────────────┘
288    (ennreal.continuous_inv.tendsto a).comp⟩
id      └────────────────────┘└──────┘  └──┘
src     └────────────────────┘└──────┘   └──┘
typ     └────────────────────┘└──────┘  └──┘
289  
290  protected lemma tendsto_inv_nat_nhds_zero : tendsto (λ n : ℕ, (n : ennreal)⁻¹) at_top (𝓝 0) :=
id                                               └─────┘              └─────┘ └┘  └────┘  
src                                              └─────┘               └─────┘ └┘  └────┘  
typ                                              └─────┘              └─────┘ └┘  └────┘  
doc                                              └─────┘                └─────┘     └────┘  
291  ennreal.inv_top ▸ ennreal.tendsto_inv_iff.2 tendsto_nat_nhds_top
id   └─────────────┘  └─────────────────────┘  └──────────────────┘
src  └─────────────┘  └─────────────────────┘  └──────────────────┘
typ  └─────────────┘  └─────────────────────┘  └──────────────────┘
292  
293  lemma Sup_add {s : set ennreal} (hs : s.nonempty) : Sup s + a = ⨆b∈s, b + a :=
id                      └─┘ └─────┘        └───────┘    └─┘         
src                     └─┘ └─────┘         └───────┘    └─┘             
typ                     └─┘ └─────┘        └───────┘    └─┘         
doc                         └─────┘         └───────┘    └─┘            
294  have Sup ((λb, b + a) '' s) = Sup s + a,
id        └─┘          └┘    └─┘   
src       └─┘             └┘     └─┘   
typ       └─┘          └┘    └─┘   
doc       └─┘                      └─┘
295    from is_lub_iff_Sup_eq.mp $ is_lub_of_is_lub_of_tendsto
id          └───────────────┘└─┘   └─────────────────────────┘
src         └───────────────┘└─┘   └─────────────────────────┘
typ         └───────────────┘└─┘   └─────────────────────────┘
296      (assume x _ y _ h, add_le_add' h (le_refl _))
id                     └─────────┘   └─────┘
src                         └─────────┘    └─────┘
typ                    └─────────┘   └─────┘
297      is_lub_Sup
id       └────────┘
src      └────────┘
typ      └────────┘
298      hs
id       └┘
typ      └┘
299      (tendsto.add (tendsto_id' inf_le_left) tendsto_const_nhds),
id        └─────────┘  └─────────┘ └─────────┘  └────────────────┘
src       └─────────┘  └─────────┘ └─────────┘  └────────────────┘
typ       └─────────┘  └─────────┘ └─────────┘  └────────────────┘
300  by simp [Sup_image, -add_comm] at this; exact this.symm
id            └───────┘                            └───────┘
src     └────┘└───────┘└──────────────────┘  └────┘└───────┘
typ     └────┘└───────┘└──────────────────┘  └────┘└───────┘
doc     └────┘         └──────────────────┘  └────┘         
txt     └────┘         └──────────────────┘  └────┘         
par     └────┘         └──────────────────┘  └────┘         
pid                  └──────────┘└─────┘                
st     └─────────────────────────────────────────────────────
301  
src  
typ  
doc  
txt  
par  
pid  
st   
302  lemma supr_add {ι : Sort*} {s : ι → ennreal} [h : nonempty ι] : supr s + a = ⨆b, s b + a :=
id                                      └─────┘       └──────┘     └──┘         
src                                      └─────┘       └──────┘      └──┘             
typ                                     └─────┘       └──────┘     └──┘         
doc                                      └─────┘                     └──┘          
303  let ⟨x⟩ := h in
id   └─┘       
typ  └─┘       
304  calc supr s + a = Sup (range s) + a : by simp [Sup_range]
id        └──┘      └─┘  └───┘                └───────┘
src       └──┘        └─┘  └───┘            └────┘└───────┘└─
typ       └──┘      └─┘  └───┘          └────┘└───────┘└─
doc       └──┘         └─┘  └───┘             └────┘         └─
txt                                           └────┘         └─
par                                           └────┘         └─
pid                                                        
st                                           └─────────────────
305    ... = (⨆b∈range s, b + a) : Sup_add ⟨s x, x, rfl⟩
id             └───┘        └─────┘         └─┘
src  ─┘         └───┘           └─────┘          └─┘
typ  ─┘        └───┘        └─────┘         └─┘
doc  ─┘         └───┘  
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
306    ... = _ : supr_range
id               └────────┘
src              └────────┘
typ              └────────┘
307  
308  lemma add_supr {ι : Sort*} {s : ι → ennreal} [h : nonempty ι] : a + supr s = ⨆b, a + s b :=
id                                      └─────┘       └──────┘       └──┘       
src                                      └─────┘       └──────┘         └──┘        
typ                                     └─────┘       └──────┘       └──┘       
doc                                      └─────┘                         └──┘      
309  by rw [add_comm, supr_add]; simp
id          └──────┘  └──────┘
src     └──┘└──────┘└┘└──────┘  └────
typ     └──┘└──────┘└┘└──────┘  └────
doc     └──┘        └┘          └────
txt     └──┘        └┘          └────
par     └──┘        └┘          └────
pid       └┘        └┘              
st     └───────────┘└────────┘└──────
310  
src  
typ  
doc  
txt  
par  
pid  
st   
311  lemma supr_add_supr {ι : Sort*} {f g : ι → ennreal} (h : ∀i j, ∃k, f i + g j ≤ f k + g k) :
id                                             └─────┘                      
src                                             └─────┘                             
typ                                            └─────┘                      
doc                                             └─────┘
312    supr f + supr g = (⨆ a, f a + g a) :=
id     └──┘   └──┘          
src    └──┘    └──┘            
typ    └──┘   └──┘          
doc    └──┘     └──┘        
313  begin
st   └─────
314    by_cases hι : nonempty ι,
id                   └──────┘ 
src    └───────┘  └─┘└──────┘
typ    └───────┘  └─┘└──────┘
doc    └───────┘  └─┘        
txt    └───────┘  └─┘        
par    └───────┘  └─┘        
pid              └─┘        
st   ─────────────────────────┘└─
315    { letI := hι,
id               └┘
src      └──────┘
typ      └──────┘└┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid          └─┘
st   ───┘└────────┘└─
316      refine le_antisymm _ (supr_le $ λ a, add_le_add' (le_supr _ _) (le_supr _ _)),
id              └─────────┘    └─────┘        └─────────┘                └─────┘
src      └─────┘└─────────┘└─┘ └─────┘  └──┘└─────────┘        └────┘ └─────┘└────┘
typ      └─────┘└─────────┘└─┘ └─────┘  └──┘└─────────┘        └────┘ └─────┘└────┘
doc      └─────┘           └─┘          └──┘                   └────┘        └────┘
txt      └─────┘           └─┘          └──┘                   └────┘        └────┘
par      └─────┘           └─┘          └──┘                   └────┘        └────┘
pid                       └─┘          └──┘                   └────┘        └────┘
st   ────────────────────────────────────────────────────────────────────────────────┘└─
317      simpa [add_supr, supr_add] using
id              └──────┘  └──────┘
src      └─────┘└──────┘└┘└──────┘└───────
typ      └─────┘└──────┘└┘└──────┘└───────
doc      └─────┘        └┘        └───────
txt      └─────┘        └┘        └───────
par      └─────┘        └┘        └───────
pid                   └┘        └─────
st   ─────────────────────────────────────
318        λ i j:ι, show f i + g j ≤ ⨆ a, f a + g a, from
id                                        
src  ─────┘ └───┘ └┘        └┘     └──────
typ  ─────┘ └───┘└┘        └┘   └──────
doc  ─────┘ └───┘ └┘          └┘     └──────
txt  ─────┘ └───┘ └┘           └┘      └──────
par  ─────┘ └───┘ └┘           └┘      └──────
pid  ─────┘ └───┘ └┘           └┘      └──────
st   ─────────────────────────────────────────────────────
319        let ⟨k, hk⟩ := h i j in le_supr_of_le k hk },
id                └┘             └───────────┘
src  ─────┘     └┘  └───┘   └──┘└───────────┘   
typ  ─────┘    └┘└┘└───┘  └──┘└───────────┘   
doc  ─────┘     └┘  └───┘   └──┘                
txt  ─────┘     └┘  └───┘   └──┘                
par  ─────┘     └┘  └───┘   └──┘                
pid  ─────┘     └┘  └───┘   └──┘                
st   ────────────────────────────────────────────────┘└┘
320    { have : ∀f:ι → ennreal, (⨆i, f i) = 0 := assume f, bot_unique (supr_le $ assume i, (hι ⟨i⟩).elim),
id                    └─────┘                          └────────┘  └─────┘              └┘
src      └─────┘ └┘  └─────┘    └┘└────┘      └──┘└────────┘ └─────┘       └──┘     └──────┘
typ      └─────┘ └┘ └─────┘    └┘└────┘      └──┘└────────┘ └─────┘       └──┘ └┘  └──────┘
doc      └─────┘ └┘  └─────┘    └┘ └────┘      └──┘                         └──┘     └──────┘
txt      └─────┘ └┘               └┘ └────┘      └──┘                         └──┘     └──────┘
par      └─────┘ └┘               └┘ └────┘      └──┘                         └──┘     └──────┘
pid      └───┘└┘ └┘               └┘ └───┘      └──┘                         └──┘     └──────┘
st   ───────────────────────────────────────────────────────────────────────────────────────────────────┘└─
321      rw [this, this, this, zero_add] }
id           └──┘  └──┘  └──┘  └──────┘
src      └──┘    └┘    └┘    └┘└──────┘└┘
typ      └──┘└──┘└┘└──┘└┘└──┘└┘└──────┘└┘
doc      └──┘    └┘    └┘    └┘        └┘
txt      └──┘    └┘    └┘    └┘        └┘
par      └──┘    └┘    └┘    └┘        └┘
pid        └┘    └┘    └┘    └┘        
st   ───────────┘└────┘└────┘└────────┘└─
322  end
st   ──┘
323  
324  lemma supr_add_supr_of_monotone {ι : Sort*} [semilattice_sup ι]
id                                                └─────────────┘ 
src                                               └─────────────┘
typ                                               └─────────────┘ 
doc                                               └─────────────┘
325    {f g : ι → ennreal} (hf : monotone f) (hg : monotone g) :
id               └─────┘        └──────┘         └──────┘ 
src               └─────┘        └──────┘          └──────┘
typ              └─────┘        └──────┘         └──────┘ 
doc               └─────┘        └──────┘          └──────┘
326    supr f + supr g = (⨆ a, f a + g a) :=
id     └──┘   └──┘          
src    └──┘    └──┘            
typ    └──┘   └──┘          
doc    └──┘     └──┘        
327  supr_add_supr $ assume i j, ⟨i ⊔ j, add_le_add' (hf $ le_sup_left) (hg $ le_sup_right)⟩
id   └───────────┘                  └─────────┘  └┘   └─────────┘   └┘   └──────────┘
src  └───────────┘                      └─────────┘       └─────────┘        └──────────┘
typ  └───────────┘                  └─────────┘  └┘   └─────────┘   └┘   └──────────┘
328  
329  lemma finset_sum_supr_nat {α} {ι} [semilattice_sup ι] {s : finset α} {f : α → ι → ennreal}
id                                      └─────────────┘        └────┘              └─────┘
src                                     └─────────────┘         └────┘                 └─────┘
typ                                     └─────────────┘        └────┘              └─────┘
doc                                     └─────────────┘         └────┘                 └─────┘
330    (hf : ∀a, monotone (f a)) :
id              └──────┘   
src              └──────┘
typ             └──────┘   
doc              └──────┘
331    s.sum (λa, supr (f a)) = (⨆ n, s.sum (λa, f a n)) :=
id     └──┘     └──┘          └──┘       
src     └──┘      └──┘              └──┘
typ    └──┘     └──┘          └──┘       
doc               └──┘             
332  begin
st   └─────
333    refine finset.induction_on s _ _,
id            └─────────────────┘ 
src    └─────┘└─────────────────┘ └──┘
typ    └─────┘└─────────────────┘└──┘
doc    └─────┘└─────────────────┘ └──┘
txt    └─────┘                    └──┘
par    └─────┘                    └──┘
pid                              └──┘
st   ─────────────────────────────────┘└─
334    { simp,
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
st   ───┘└──┘└─
335      exact (bot_unique $ supr_le $ assume i, le_refl ⊥).symm },
id              └────────┘   └─────┘             └─────┘ 
src      └────┘ └────────┘ └─────┘       └──┘└─────┘└─────┘
typ      └────┘ └────────┘ └─────┘       └──┘└─────┘└─────┘
doc      └────┘                          └──┘        └─────┘
txt      └────┘                          └──┘        └─────┘
par      └────┘                          └──┘        └─────┘
pid                                     └──┘        └───┘└┘
st   ───────────────────────────────────────────────────────────┘└┘
336    { assume a s has ih,
src      └───────────────┘
typ      └───────────────┘
doc      └───────────────┘
txt      └───────────────┘
par      └───────────────┘
pid      └───────────────┘
st   ────────────────────┘└─
337      simp only [finset.sum_insert has],
id                  └───────────────┘ └─┘
src      └─────────┘└───────────────┘   
typ      └─────────┘└───────────────┘└─┘
doc      └─────────┘                    
txt      └─────────┘                    
par      └─────────┘                    
pid          └──┘└┘                    
st   ────────────────────────────────────┘└─
338      rw [ih, supr_add_supr_of_monotone (hf a)],
id           └┘  └───────────────────────┘  └┘ 
src      └──┘  └┘└───────────────────────┘    └┘
typ      └──┘└┘└┘└───────────────────────┘ └┘└┘
doc      └──┘  └┘                             └┘
txt      └──┘  └┘                             └┘
par      └──┘  └┘                             └┘
pid        └┘  └┘                             └┘
st   ─────────┘└────────────────────────────────┘└──
339      assume i j h,
src      └──────────┘
typ      └──────────┘
doc      └──────────┘
txt      └──────────┘
par      └──────────┘
pid      └──────────┘
st   ───────────────┘└─
340      exact (finset.sum_le_sum $ assume a ha, hf a h) }
id              └───────────────┘                └┘   
src      └────┘ └───────────────┘       └─────┘    └┘
typ      └────┘ └───────────────┘       └─────┘└┘ └┘
doc      └────┘                         └─────┘    └┘
txt      └────┘                         └─────┘    └┘
par      └────┘                         └─────┘    └┘
pid                                    └─────┘    
st   ───────────────────────────────────────────────────┘└─
341  end
st   ──┘
342  
343  section priority
344  -- for some reason the next proof fails without changing the priority of this instance
345  local attribute [instance, priority 1000] classical.prop_decidable
id                                             └──────────────────────┘
src                                            └──────────────────────┘
typ                                            └──────────────────────┘
346  lemma mul_Sup {s : set ennreal} {a : ennreal} : a * Sup s = ⨆i∈s, a * i :=
id                      └─┘ └─────┘       └─────┘      └─┘       
src                     └─┘ └─────┘       └─────┘       └─┘          
typ                     └─┘ └─────┘       └─────┘      └─┘       
doc                         └─────┘       └─────┘        └─┘        
347  begin
st   └─────
348    by_cases hs : ∀x∈s, x = (0:ennreal),
id                              └─────┘
src    └───────┘  └─┘ └┘    └┘└─────┘
typ    └───────┘  └─┘ └┘   └┘└─────┘
doc    └───────┘  └─┘ └┘     └┘└─────┘
txt    └───────┘  └─┘ └┘     └┘       
par    └───────┘  └─┘ └┘     └┘       
pid              └─┘ └┘     └┘       
st   ────────────────────────────────────┘└─
349    { have h₁ : Sup s = 0 := (bot_unique $ Sup_le $ assume a ha, (hs a ha).symm ▸ le_refl 0),
id                 └─┘          └────────┘   └────┘                 └┘             └─────┘
src      └────────┘└─┘  └────┘ └────────┘ └────┘       └─────┘      └─────┘└─────┘└─┘
typ      └────────┘└─┘ └────┘ └────────┘ └────┘       └─────┘ └┘   └─────┘└─────┘└─┘
doc      └────────┘└─┘  └────┘                         └─────┘      └─────┘        └─┘
txt      └────────┘     └────┘                         └─────┘      └─────┘        └─┘
par      └────────┘     └────┘                         └─────┘      └─────┘        └─┘
pid      └─────┘└─┘     └───┘                         └─────┘      └─────┘        └─┘
st   ───┘└────────────────────────────────────────────────────────────────────────────────────┘└─
350      have h₂ : (⨆i ∈ s, a * i) = 0 :=
id                        
src      └────────┘ └──┘   └┘ └─────
typ      └────────┘ └──┘ └┘ └─────
doc      └────────┘ └──┘    └┘ └─────
txt      └────────┘  └──┘     └┘ └─────
par      └────────┘  └──┘     └┘ └─────
pid      └─────┘└─┘  └──┘     └┘ └────
st   ─────────────────────────────────────
351        (bot_unique $ supr_le $ assume a, supr_le $ assume ha, by simp [hs a ha]),
id          └────────┘                       └─────┘                       └┘  └┘
src  ─────┘ └────────┘               └──┘└─────┘       └───┘  └────┘     
typ  ─────┘ └────────┘               └──┘└─────┘       └───┘  └────┘└┘└┘
doc  ─────┘                          └──┘              └───┘  └────┘     
txt  ─────┘                          └──┘              └───┘  └────┘     
par  ─────┘                          └──┘              └───┘  └────┘     
pid  ─────┘                          └──┘              └───┘  └─────┘     └┘
st   ──────────────────────────────────────────────────────────────┘└─────────────┘└─
352      rw [h₁, h₂, mul_zero] },
id           └┘  └┘  └──────┘
src      └──┘  └┘  └┘└──────┘└┘
typ      └──┘└┘└┘└┘└┘└──────┘└┘
doc      └──┘  └┘  └┘        └┘
txt      └──┘  └┘  └┘        └┘
par      └──┘  └┘  └┘        └┘
pid        └┘  └┘  └┘        
st   ─────────┘└──┘└────────┘└┘
353    { simp only [not_forall] at hs,
id                  └────────┘
src      └─────────┘└────────┘└─────┘
typ      └─────────┘└────────┘└─────┘
doc      └─────────┘          └─────┘
txt      └─────────┘          └─────┘
par      └─────────┘          └─────┘
pid          └──┘└┘          └───┘
st   ───────────────────────────────┘└─
354      rcases hs with ⟨x, hx, hx0⟩,
id              └┘
src      └─────┘  └────────────────┘
typ      └─────┘└┘└────────────────┘
doc      └─────┘  └────────────────┘
txt      └─────┘  └────────────────┘
par      └─────┘  └────────────────┘
pid              └────────────────┘
st   ──────────────────────────────┘└─
355      have s₁ : Sup s ≠ 0 :=
id                 └─┘  
src      └────────┘└─┘ └─────
typ      └────────┘└─┘└─────
doc      └────────┘└─┘  └─────
txt      └────────┘     └─────
par      └────────┘     └─────
pid      └─────┘└─┘     └────
st   ───────────────────────────
356        zero_lt_iff_ne_zero.1 (lt_of_lt_of_le (zero_lt_iff_ne_zero.2 hx0) (le_Sup hx)),
id                                └────────────┘  └─────────────────┘   └─┘   └────┘ └┘
src  ─────┘                   └─┘ └────────────┘ └─────────────────┘└─┘   └┘ └────┘  └┘
typ  ─────┘                   └─┘ └────────────┘ └─────────────────┘└─┘└─┘└┘ └────┘└┘└┘
doc  ─────┘                   └─┘                                   └─┘   └┘         └┘
txt  ─────┘                   └─┘                                   └─┘   └┘         └┘
par  ─────┘                   └─┘                                   └─┘   └┘         └┘
pid  ─────┘                   └─┘                                   └─┘   └┘         └┘
st   ───────────────────────────────────────────────────────────────────────────────────┘└─
357      have : Sup ((λb, a * b) '' s) = a * Sup s :=
id                               └┘         └─┘ 
src      └─────┘      └─┘   └┘└┘ └┘   └─┘ └───
typ      └─────┘      └─┘   └┘└┘ └┘  └─┘└───
doc      └─────┘      └─┘   └┘   └┘   └─┘ └───
txt      └─────┘      └─┘   └┘   └┘       └───
par      └─────┘      └─┘   └┘   └┘       └───
pid      └───┘└┘      └─┘   └┘   └┘       └───
st   ─────────────────────────────────────────────────
358        is_lub_iff_Sup_eq.mp (is_lub_of_is_lub_of_tendsto
id         └──────────────────┘  └─────────────────────────┘
src  ─────┘└──────────────────┘ └─────────────────────────┘
typ  ─────┘└──────────────────┘ └─────────────────────────┘
doc  ─────┘                                                
txt  ─────┘                                                
par  ─────┘                                                
pid  ─────┘                                                
st   ────────────────────────────────────────────────────────
359          (assume x _ y _ h, canonically_ordered_semiring.mul_le_mul (le_refl _) h)
id                              └─────────────────────────────────────┘  └─────┘
src  ───────┘       └──────────┘└─────────────────────────────────────┘ └─────┘└──┘ └─
typ  ───────┘       └──────────┘└─────────────────────────────────────┘ └─────┘└──┘ └─
doc  ───────┘       └──────────┘                                               └──┘ └─
txt  ───────┘       └──────────┘                                               └──┘ └─
par  ───────┘       └──────────┘                                               └──┘ └─
pid  ───────┘       └──────────┘                                               └──┘ └─
st   ──────────────────────────────────────────────────────────────────────────────────
360          is_lub_Sup
id           └────────┘
src  ───────┘└────────┘
typ  ───────┘└────────┘
doc  ───────┘          
txt  ───────┘          
par  ───────┘          
pid  ───────┘          
st   ───────────────────
361          ⟨x, hx⟩
id              └┘
src  ───────┘  └┘  └─
typ  ───────┘ └┘└┘└─
doc  ───────┘  └┘  └─
txt  ───────┘  └┘  └─
par  ───────┘  └┘  └─
pid  ───────┘  └┘  └─
st   ────────────────
362          (ennreal.tendsto.const_mul (tendsto_id' inf_le_left) (or.inl s₁))),
id            └───────────────────────┘  └─────────┘ └─────────┘   └────┘ └┘
src  ───────┘ └───────────────────────┘ └─────────┘└─────────┘└┘ └────┘  └─┘
typ  ───────┘ └───────────────────────┘ └─────────┘└─────────┘└┘ └────┘└┘└─┘
doc  ───────┘                                                 └┘         └─┘
txt  ───────┘                                                 └┘         └─┘
par  ───────┘                                                 └┘         └─┘
pid  ───────┘                                                 └┘         └─┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
363      rw [this.symm, Sup_image] }
id                      └───────┘
src      └──┘         └┘└───────┘└┘
typ      └──┘└───────┘└┘└───────┘└┘
doc      └──┘         └┘         └┘
txt      └──┘         └┘         └┘
par      └──┘         └┘         └┘
pid        └┘         └┘         
st   ────────────────┘└─────────┘└─
364  end
st   ──┘
365  end priority
366  
367  lemma mul_supr {ι : Sort*} {f : ι → ennreal} {a : ennreal} : a * supr f = ⨆i, a * f i :=
id                                      └─────┘       └─────┘      └──┘       
src                                      └─────┘       └─────┘       └──┘        
typ                                     └─────┘       └─────┘      └──┘       
doc                                      └─────┘       └─────┘        └──┘      
368  by rw [← Sup_range, mul_Sup, supr_range]
id            └───────┘  └─────┘  └────────┘
src     └────┘└───────┘└┘└─────┘└┘└────────┘└─
typ     └────┘└───────┘└┘└─────┘└┘└────────┘└─
doc     └────┘         └┘       └┘          └─
txt     └────┘         └┘       └┘          └─
par     └────┘         └┘       └┘          └─
pid       └──┘         └┘       └┘          
st     └──────────────┘└───────┘└──────────┘
369  
src  
typ  
doc  
txt  
par  
pid  
st   
370  lemma supr_mul {ι : Sort*} {f : ι → ennreal} {a : ennreal} : supr f * a = ⨆i, f i * a :=
id                                      └─────┘       └─────┘    └──┘         
src                                      └─────┘       └─────┘    └──┘             
typ                                     └─────┘       └─────┘    └──┘         
doc                                      └─────┘       └─────┘    └──┘          
371  by rw [mul_comm, mul_supr]; congr; funext; rw [mul_comm]
id          └──────┘  └──────┘                      └──────┘
src     └──┘└──────┘└┘└──────┘  └───┘  └────┘  └──┘└──────┘└─
typ     └──┘└──────┘└┘└──────┘  └───┘  └────┘  └──┘└──────┘└─
doc     └──┘        └┘                 └────┘  └──┘        └─
txt     └──┘        └┘          └───┘  └────┘  └──┘        └─
par     └──┘        └┘          └───┘  └────┘  └──┘        └─
pid       └┘        └┘                           └┘        
st     └───────────┘└────────┘└───────────────────┘└──────┘
372  
src  
typ  
doc  
txt  
par  
pid  
st   
373  protected lemma tendsto_coe_sub : ∀{b:ennreal}, tendsto (λb:ennreal, ↑r - b) (𝓝 b) (𝓝 (↑r - b)) :=
id                                         └─────┘   └─────┘     └─────┘               
src                                        └─────┘   └─────┘     └─────┘                  
typ                                        └─────┘   └─────┘     └─────┘               
doc                                        └─────┘   └─────┘     └─────┘                
374  begin
st   └─────
375    refine (forall_ennreal.2 $ and.intro (assume a, _) _),
id             └────────────┘     └───────┘
src    └─────┘ └────────────┘└─┘ └───────┘       └───────┘
typ    └─────┘ └────────────┘└─┘ └───────┘       └───────┘
doc    └─────┘               └─┘                 └───────┘
txt    └─────┘               └─┘                 └───────┘
par    └─────┘               └─┘                 └───────┘
pid                         └─┘                 └───────┘
st   ──────────────────────────────────────────────────────┘└─
376    { simp [@nhds_coe a, tendsto_map'_iff, (∘), tendsto_coe, coe_sub.symm],
id              └──────┘   └──────────────┘      └─────────┘
src      └────┘ └──────┘ └┘└──────────────┘└┘└──┘└─────────┘└┘            
typ      └────┘ └──────┘└┘└──────────────┘└┘└──┘└─────────┘└┘└──────────┘
doc      └────┘          └┘                └┘ └──┘           └┘            
txt      └────┘          └┘                └┘ └──┘           └┘            
par      └────┘          └┘                └┘ └──┘           └┘            
pid                    └┘                └┘ └──┘           └┘            
st   ───┘└──────────────────────────────────────────────────────────────────┘└─
377      exact nnreal.tendsto.sub tendsto_const_nhds tendsto_id },
id             └────────────────┘ └────────────────┘ └────────┘
src      └────┘└────────────────┘└────────────────┘└────────┘
typ      └────┘└────────────────┘└────────────────┘└────────┘
doc      └────┘                                              
txt      └────┘                                              
par      └────┘                                              
pid                                                         
st   ──────────────────────────────────────────────────────────┘└┘
378    simp,
src    └──┘
typ    └──┘
doc    └──┘
txt    └──┘
par    └──┘
st   ─────┘└─
379    exact (tendsto.congr' (mem_sets_of_superset (lt_mem_nhds $ @coe_lt_top r) $
id            └────────────┘  └──────────────────┘  └─────────┘    └────────┘ 
src    └────┘ └────────────┘ └──────────────────┘ └─────────┘  └────────┘ └┘ 
typ    └────┘ └────────────┘ └──────────────────┘ └─────────┘  └────────┘└┘ 
doc    └────┘                                                             └┘ 
txt    └────┘                                                             └┘ 
par    └────┘                                                             └┘ 
pid                                                                      └┘ 
st   ──────────────────────────────────────────────────────────────────────────────
380      by simp [le_of_lt] {contextual := tt})) tendsto_const_nhds
id                └──────┘                 └┘    └────────────────┘
src  ───┘  └────┘└──────┘└┘ └────────────┘└┘└─┘└────────────────┘
typ  ───┘  └────┘└──────┘└┘ └────────────┘└┘└─┘└────────────────┘
doc  ───┘  └────┘        └┘ └────────────┘  └─┘                  
txt  ───┘  └────┘        └┘ └────────────┘  └─┘                  
par  ───┘  └────┘        └┘ └────────────┘  └─┘                  
pid  ───┘  └─────┘        └┘ └────────────┘  └──┘                  
st   ─────┘└─────────────────────────────────┘└────────────────────┘
381  end
st   └─┘
382  
383  lemma sub_supr {ι : Sort*} [hι : nonempty ι] {b : ι → ennreal} (hr : a < ⊤) :
id                                    └──────┘           └─────┘          
src                                   └──────┘             └─────┘           
typ                                   └──────┘           └─────┘          
doc                                                        └─────┘
384    a - (⨆i, b i) = (⨅i, a - b i) :=
id                  
src                     
typ                 
doc                    
385  let ⟨i⟩ := hι in
id   └─┘       └┘
typ  └─┘       └┘
386  let ⟨r, eq, _⟩ := lt_iff_exists_coe.mp hr in
id   └─┘              └───────────────┘└─┘ └┘
src                    └───────────────┘└─┘
typ  └─┘              └───────────────┘└─┘ └┘
387  have Inf ((λb, ↑r - b) '' range b) = ↑r - (⨆i, b i),
id        └─┘           └┘ └───┘          
src       └─┘             └┘ └───┘          
typ       └─┘           └┘ └───┘          
doc       └─┘                  └───┘             
388    from is_glb_iff_Inf_eq.mp $ is_glb_of_is_lub_of_tendsto
id          └───────────────┘└─┘   └─────────────────────────┘
src         └───────────────┘└─┘   └─────────────────────────┘
typ         └───────────────┘└─┘   └─────────────────────────┘
389      (assume x _ y _, sub_le_sub (le_refl _))
id                    └────────┘  └─────┘
src                       └────────┘  └─────┘
typ                   └────────┘  └─────┘
390      is_lub_supr
id       └─────────┘
src      └─────────┘
typ      └─────────┘
391      ⟨_, i, rfl⟩
id              └─┘
src             └─┘
typ             └─┘
392      (tendsto.comp ennreal.tendsto_coe_sub (tendsto_id' inf_le_left)),
id        └──────────┘ └─────────────────────┘  └─────────┘ └─────────┘
src       └──────────┘ └─────────────────────┘  └─────────┘ └─────────┘
typ       └──────────┘ └─────────────────────┘  └─────────┘ └─────────┘
393  by rw [eq, ←this]; simp [Inf_image, infi_range, -mem_range]; exact le_refl _
id          └┘   └──┘         └───────┘  └────────┘
src     └──┘└┘└─┘      └────┘└───────┘└┘└────────┘└───────────┘  └────┘       └──
typ     └──┘└┘└─┘└──┘  └────┘└───────┘└┘└────────┘└───────────┘  └────┘       └──
doc     └──┘  └─┘      └────┘         └┘          └───────────┘  └────┘       └──
txt     └──┘  └─┘      └────┘         └┘          └───────────┘  └────┘       └──
par     └──┘  └─┘      └────┘         └┘          └───────────┘  └────┘       └──
pid       └┘  └─┘                   └┘          └───────────┘              └┘
st     └─────┘└─────┘└───────────────────────────────────────────────────────────
394  
src  
typ  
doc  
txt  
par  
pid  
st   
395  end topological_space
396  
397  section tsum
398  
399  variables {f g : α → ennreal}
id                        └─────┘
src                       └─────┘
typ                       └─────┘
doc                       └─────┘
400  
401  @[elim_cast] protected lemma has_sum_coe {f : α → nnreal} {r : nnreal} :
id                                                    └────┘       └────┘
src                                                    └────┘       └────┘
typ                                                   └────┘       └────┘
doc    └───────┘                                       └────┘       └────┘
402    has_sum (λa, (f a : ennreal)) ↑r ↔ has_sum f r :=
id     └─────┘          └─────┘     └─────┘  
src    └─────┘             └─────┘      └─────┘
typ    └─────┘          └─────┘     └─────┘  
doc    └─────┘             └─────┘        └─────┘
403  have (λs:finset α, s.sum (coe ∘ f)) = (coe : nnreal → ennreal) ∘ (λs:finset α, s.sum f),
id            └────┘   └──┘  └─┘       └─┘   └────┘   └─────┘       └────┘   └──┘ 
src           └────┘     └──┘  └─┘        └─┘   └────┘   └─────┘       └────┘     └──┘
typ           └────┘   └──┘  └─┘       └─┘   └────┘   └─────┘       └────┘   └──┘ 
doc           └────┘                              └────┘   └─────┘        └────┘
404    from funext $ assume s, ennreal.coe_finset_sum.symm,
id          └────┘            └────────────────────┘└───┘
src         └────┘             └────────────────────┘└───┘
typ         └────┘            └────────────────────┘└───┘
405  by unfold has_sum; rw [this, tendsto_coe]
id                          └──┘  └─────────┘
src     └────────────┘  └──┘    └┘└─────────┘└─
typ     └────────────┘  └──┘└──┘└┘└─────────┘└─
doc     └────────────┘  └──┘    └┘           └─
txt     └────────────┘  └──┘    └┘           └─
par     └────────────┘  └──┘    └┘           └─
pid           └──────┘    └┘    └┘           
st     └───────────────────┘└──┘└───────────┘
406  
src  
typ  
doc  
txt  
par  
pid  
st   
407  protected lemma tsum_coe_eq {f : α → nnreal} (h : has_sum f r) : (∑a, (f a : ennreal)) = r :=
id                                       └────┘       └─────┘             └─────┘    
src                                       └────┘       └─────┘                  └─────┘   
typ                                      └────┘       └─────┘             └─────┘    
doc                                       └────┘       └─────┘                  └─────┘
408  tsum_eq_has_sum $ ennreal.has_sum_coe.2 $ h
id   └─────────────┘   └─────────────────┘    
src  └─────────────┘   └─────────────────┘
typ  └─────────────┘   └─────────────────┘    
409  
410  protected lemma coe_tsum {f : α → nnreal} : summable f → ↑(tsum f) = (∑a, (f a : ennreal))
id                                    └────┘    └──────┘    └──┘           └─────┘
src                                    └────┘    └──────┘      └──┘               └─────┘
typ                                   └────┘    └──────┘    └──┘           └─────┘
doc                                    └────┘    └──────┘       └──┘                └─────┘
411  | ⟨r, hr⟩ := by rw [tsum_eq_has_sum hr, ennreal.tsum_coe_eq hr]
id                       └─────────────┘ └┘  └─────────────────┘ └┘
src                  └──┘└─────────────┘  └┘└─────────────────┘  └─
typ                  └──┘└─────────────┘└┘└┘└─────────────────┘└┘└─
doc                  └──┘                 └┘                     └─
txt                  └──┘                 └┘                     └─
par                  └──┘                 └┘                     └─
pid                    └┘                 └┘                     
st                  └─────────────────────┘└──────────────────────┘
412  
src  
typ  
doc  
txt  
par  
pid  
st   
413  protected lemma has_sum : has_sum f (⨆s:finset α, s.sum f) :=
id                             └─────┘     └────┘  └──┘ 
src                            └─────┘      └────┘    └──┘
typ                            └─────┘     └────┘  └──┘ 
doc                            └─────┘      └────┘  
414  tendsto_order.2
id   └───────────┘
src  └───────────┘
typ  └───────────┘
415    ⟨assume a' ha',
id             └┘ └─┘
typ            └┘ └─┘
416      let ⟨s, hs⟩ := lt_supr_iff.mp ha' in
id       └─┘    └┘     └─────────┘└─┘ └─┘
src                     └─────────┘└─┘
typ      └─┘    └┘     └─────────┘└─┘ └─┘
417      mem_at_top_sets.mpr ⟨s, assume t ht, lt_of_lt_of_le hs $ finset.sum_le_sum_of_subset ht⟩,
id       └─────────────┘└──┘             └┘  └────────────┘      └─────────────────────────┘ └┘
src      └─────────────┘└──┘                  └────────────┘      └─────────────────────────┘
typ      └─────────────┘└──┘             └┘  └────────────┘      └─────────────────────────┘ └┘
418    assume a' ha',
id            └┘ └─┘
typ           └┘ └─┘
419      univ_mem_sets' $ assume s,
id       └────────────┘          
src      └────────────┘
typ      └────────────┘          
420      have s.sum f ≤ ⨆(s : finset α), s.sum f,
id            └──┘        └────┘   └──┘ 
src            └──┘         └────┘     └──┘
typ           └──┘        └────┘   └──┘ 
doc                          └────┘   
421        from le_supr (λ(s : finset α), s.sum f) s,
id              └─────┘        └────┘    └──┘   
src             └─────┘        └────┘      └──┘
typ             └─────┘        └────┘    └──┘   
doc                            └────┘
422      lt_of_le_of_lt this ha'⟩
id       └────────────┘ └──┘ └─┘
src      └────────────┘
typ      └────────────┘ └──┘ └─┘
423  
424  @[simp] protected lemma summable : summable f := ⟨_, ennreal.has_sum⟩
id                                      └──────┘         └─────────────┘
src                                     └──────┘          └─────────────┘
typ                                     └──────┘         └─────────────┘
doc    └──┘                             └──────┘
425  
426  lemma tsum_coe_ne_top_iff_summable {f : β → nnreal} :
id                                              └────┘
src                                              └────┘
typ                                             └────┘
doc                                              └────┘
427    (∑ b, (f b:ennreal)) ≠ ∞ ↔ summable f :=
id           └─────┘      └──────┘ 
src             └─────┘      └──────┘
typ          └─────┘      └──────┘ 
doc             └─────┘        └──────┘
428  begin
st   └─────
429    refine ⟨λ h, _, λ h, ennreal.coe_tsum h ▸ ennreal.coe_ne_top⟩,
id                          └──────────────┘    └────────────────┘
src    └─────┘  └─────┘ └──┘└──────────────┘ └────────────────┘
typ    └─────┘  └─────┘ └──┘└──────────────┘ └────────────────┘
doc    └─────┘  └─────┘ └──┘                                    
txt    └─────┘  └─────┘ └──┘                                    
par    └─────┘  └─────┘ └──┘                                    
pid            └─────┘ └──┘                                    
st   ──────────────────────────────────────────────────────────────┘└─
430    lift (∑ b, (f b:ennreal)) to nnreal using h with a ha,
id                  └─────┘      └────┘       
src    └───┘ └┘   └─────┘└────┘└────┘└─────┘ └────────┘
typ    └───┘ └┘  └─────┘└────┘└────┘└─────┘└────────┘
doc    └───┘ └┘   └─────┘└────┘└────┘└─────┘ └────────┘
txt    └───┘  └┘           └────┘      └─────┘ └────────┘
par    └───┘  └┘           └────┘      └─────┘ └────────┘
pid          └┘           └┘└──┘      └─────┘ └────────┘
st   ──────────────────────────────────────────────────────┘└─
431    refine ⟨a, ennreal.has_sum_coe.1 _⟩,
id               └─────────────────┘
src    └─────┘  └┘└─────────────────┘└───┘
typ    └─────┘ └┘└─────────────────┘└───┘
doc    └─────┘  └┘                   └───┘
txt    └─────┘  └┘                   └───┘
par    └─────┘  └┘                   └───┘
pid            └┘                   └───┘
st   ────────────────────────────────────┘└─
432    rw ha,
id        └┘
src    └─┘
typ    └─┘└┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ──────┘└─
433    exact has_sum_tsum ennreal.summable
id           └──────────┘ └──────────────┘
src    └────┘└──────────┘└──────────────┘
typ    └────┘└──────────┘└──────────────┘
doc    └────┘                            
txt    └────┘                            
par    └────┘                            
pid                                     
st   ─────────────────────────────────────┘
434  end
st   └─┘
435  
436  protected lemma tsum_eq_supr_sum : (∑a, f a) = (⨆s:finset α, s.sum f) :=
id                                               └────┘  └──┘ 
src                                                 └────┘    └──┘
typ                                              └────┘  └──┘ 
doc                                                  └────┘  
437  tsum_eq_has_sum ennreal.has_sum
id   └─────────────┘ └─────────────┘
src  └─────────────┘ └─────────────┘
typ  └─────────────┘ └─────────────┘
438  
439  protected lemma tsum_eq_top_of_eq_top : (∃ a, f a = ∞) → (∑ a, f a) = ∞
id                                                           
src                                                                 
typ                                                          
doc                                                                     
440  | ⟨a, ha⟩ :=
441  begin
st   └─────
442    rw [ennreal.tsum_eq_supr_sum],
id         └──────────────────────┘
src    └──┘└──────────────────────┘
typ    └──┘└──────────────────────┘
doc    └──┘                        
txt    └──┘                        
par    └──┘                        
pid      └┘                        
st   ─────────────────────────────┘└──
443    apply le_antisymm le_top,
id           └─────────┘ └────┘
src    └────┘└─────────┘└────┘
typ    └────┘└─────────┘└────┘
doc    └────┘           
txt    └────┘           
par    └────┘           
pid                    
st   ─────────────────────────┘└─
444    convert le_supr (λ s:finset α, s.sum f) (finset.singleton a),
id             └─────┘      └────┘    └──┘    └──────────────┘ 
src    └──────┘└─────┘  └─┘└────┘ └┘ └──┘ └┘ └──────────────┘ 
typ    └──────┘└─────┘  └─┘└────┘└┘ └──┘└┘ └──────────────┘
doc    └──────┘         └─┘└────┘ └┘      └┘ └──────────────┘ 
txt    └──────┘         └─┘       └┘      └┘                  
par    └──────┘         └─┘       └┘      └┘                  
pid                    └─┘       └┘      └┘                  
st   ─────────────────────────────────────────────────────────────┘└─
445    rw [finset.sum_singleton, ha]
id         └──────────────────┘  └┘
src    └──┘└──────────────────┘└┘  └┘
typ    └──┘└──────────────────┘└┘└┘└┘
doc    └──┘                    └┘  └┘
txt    └──┘                    └┘  └┘
par    └──┘                    └┘  └┘
pid      └┘                    └┘  
st   ─────────────────────────┘└──┘
446  end
st   └─┘
447  
448  protected lemma ne_top_of_tsum_ne_top (h : (∑ a, f a) ≠ ∞) (a : α) : f a ≠ ∞ :=
id                                                                   
src                                                                        
typ                                                                  
doc                                                                          
449  λ ha, h $ ennreal.tsum_eq_top_of_eq_top ⟨a, ha⟩
id     └┘     └───────────────────────────┘    └┘
src            └───────────────────────────┘
typ    └┘     └───────────────────────────┘    └┘
450  
451  protected lemma tsum_sigma {β : α → Type*} (f : Πa, β a → ennreal) :
id                                                         └─────┘
src                                                            └─────┘
typ                                                        └─────┘
doc                                                            └─────┘
452    (∑p:Σa, β a, f p.1 p.2) = (∑a b, f a b) :=
id                       
src                           
typ                      
doc                                
453  tsum_sigma (assume b, ennreal.summable) ennreal.summable
id   └────────┘           └──────────────┘  └──────────────┘
src  └────────┘            └──────────────┘  └──────────────┘
typ  └────────┘           └──────────────┘  └──────────────┘
454  
455  protected lemma tsum_prod {f : α → β → ennreal} : (∑p:α×β, f p.1 p.2) = (∑a, ∑b, f a b) :=
id                                        └─────┘                    
src                                         └─────┘                        
typ                                       └─────┘                    
doc                                         └─────┘                            
456  let j : α × β → (Σa:α, β) := λp, sigma.mk p.1 p.2 in
id                           └──────┘   
src                                └──────┘     
typ                          └──────┘   
457  let i : (Σa:α, β) → α × β := λp, (p.1, p.2) in
id                              
src                                     
typ                             
458  let f' : (Σa:α, β) → ennreal := λp, f p.1 p.2 in
id                   └─────┘          
src                     └─────┘              
typ                  └─────┘          
doc                       └─────┘
459  calc (∑p:α×β, f' (j p)) = (∑p:Σa:α, β, f p.1 p.2) :
id            └┘                  
src                                        
typ           └┘                  
doc                                    
460      tsum_eq_tsum_of_iso j i (assume ⟨a, b⟩, rfl) (assume ⟨a, b⟩, rfl)
id       └─────────────────┘                  └─┘                 └─┘
src      └─────────────────┘                     └─┘                  └─┘
typ      └─────────────────┘                  └─┘                 └─┘
461     ... = (∑a, ∑b, f a b) : ennreal.tsum_sigma f
id                     └────────────────┘ 
src                         └────────────────┘
typ                    └────────────────┘ 
doc               
462  
463  protected lemma tsum_comm {f : α → β → ennreal} : (∑a, ∑b, f a b) = (∑b, ∑a, f a b) :=
id                                        └─────┘                 
src                                         └─────┘                     
typ                                       └─────┘                 
doc                                         └─────┘                      
464  let f' : α×β → ennreal := λp, f p.1 p.2 in
id              └─────┘          
src                └─────┘              
typ             └─────┘          
doc                 └─────┘
465  calc (∑a, ∑b, f a b) = (∑p:α×β, f' p) : ennreal.tsum_prod.symm
id                     └┘     └───────────────┘└───┘
src                                   └───────────────┘└───┘
typ                    └┘     └───────────────┘└───┘
doc                           
466    ... = (∑p:β×α, f' (prod.swap p)) :
id               └┘  └───────┘ 
src                    └───────┘
typ              └┘  └───────┘ 
doc                     └───────┘
467      (tsum_eq_tsum_of_iso prod.swap (@prod.swap α β) (assume ⟨a, b⟩, rfl) (assume ⟨a, b⟩, rfl)).symm
id        └─────────────────┘ └───────┘   └───────┘                   └─┘                 └─┘  └──┘
src       └─────────────────┘ └───────┘   └───────┘                      └─┘                  └─┘  └──┘
typ       └─────────────────┘ └───────┘   └───────┘                   └─┘                 └─┘  └──┘
doc                           └───────┘   └───────┘
468    ... = (∑b, ∑a, f' (prod.swap (b, a))) : @ennreal.tsum_prod β α (λb a, f' (prod.swap (b, a)))
id              └┘  └───────┘          └───────────────┘        └┘  └───────┘   
src                   └───────┘            └───────────────┘                └───────┘ 
typ             └┘  └───────┘          └───────────────┘        └┘  └───────┘   
doc                   └───────┘                                              └───────┘
469  
470  protected lemma tsum_add : (∑a, f a + g a) = (∑a, f a) + (∑a, g a) :=
id                                                
src                                                      
typ                                               
doc                                                         
471  tsum_add ennreal.summable ennreal.summable
id   └──────┘ └──────────────┘ └──────────────┘
src  └──────┘ └──────────────┘ └──────────────┘
typ  └──────┘ └──────────────┘ └──────────────┘
472  
473  protected lemma tsum_le_tsum (h : ∀a, f a ≤ g a) : (∑a, f a) ≤ (∑a, g a) :=
id                                                         
src                                                               
typ                                                        
doc                                                                 
474  tsum_le_tsum h ennreal.summable ennreal.summable
id   └──────────┘  └──────────────┘ └──────────────┘
src  └──────────┘   └──────────────┘ └──────────────┘
typ  └──────────┘  └──────────────┘ └──────────────┘
475  
476  protected lemma tsum_eq_supr_nat {f : ℕ → ennreal} :
id                                            └─────┘
src                                           └─────┘
typ                                           └─────┘
doc                                            └─────┘
477    (∑i:ℕ, f i) = (⨆i:ℕ, (finset.range i).sum f) :=
id                  └──────────┘  └─┘  
src                   └──────────┘   └─┘
typ                 └──────────┘  └─┘  
doc                      └──────────┘
478  calc _ = (⨆s:finset ℕ, s.sum f) : ennreal.tsum_eq_supr_sum
id               └────┘  └──┘     └──────────────────────┘
src              └────┘   └──┘      └──────────────────────┘
typ              └────┘  └──┘     └──────────────────────┘
doc              └────┘  
479    ... = (⨆i:ℕ, (finset.range i).sum f) : le_antisymm
id                └──────────┘  └─┘      └─────────┘
src               └──────────┘   └─┘       └─────────┘
typ               └──────────┘  └─┘      └─────────┘
doc                └──────────┘
480      (supr_le_supr2 $ assume s,
id        └───────────┘          
src       └───────────┘
typ       └───────────┘          
481        let ⟨n, hn⟩ := finset.exists_nat_subset_range s in
id         └─┘    └┘     └────────────────────────────┘ 
src                       └────────────────────────────┘
typ        └─┘    └┘     └────────────────────────────┘ 
482        ⟨n, finset.sum_le_sum_of_subset hn⟩)
id             └─────────────────────────┘
src            └─────────────────────────┘
typ            └─────────────────────────┘
483      (supr_le_supr2 $ assume i, ⟨finset.range i, le_refl _⟩)
id        └───────────┘             └──────────┘   └─────┘
src       └───────────┘              └──────────┘    └─────┘
typ       └───────────┘             └──────────┘   └─────┘
doc                                  └──────────┘
484  
485  protected lemma le_tsum (a : α) : f a ≤ (∑a, f a) :=
id                                          
src                                           
typ                                         
doc                                            
486  calc f a = ({a} : finset α).sum f : by simp
id                 └────┘  └─┘  
src                   └────┘   └─┘         └────
typ                └────┘  └─┘        └────
doc                    └────┘               └────
txt                                         └────
par                                         └────
pid                                             
st                                         └─────
487    ... ≤ (⨆s:finset α, s.sum f) : le_supr (λs:finset α, s.sum f) _
id              └────┘  └──┘     └─────┘     └────┘   └──┘ 
src  ─┘         └────┘    └──┘      └─────┘     └────┘     └──┘
typ  ─┘         └────┘  └──┘     └─────┘     └────┘   └──┘ 
doc  ─┘         └────┘                          └────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
488    ... = (∑a, f a) : by rw [ennreal.tsum_eq_supr_sum]
id                         └──────────────────────┘
src                       └──┘└──────────────────────┘└─
typ                    └──┘└──────────────────────┘└─
doc                       └──┘                        └─
txt                         └──┘                        └─
par                         └──┘                        └─
pid                           └┘                        
st                         └───────────────────────────┘
489  
src  
typ  
doc  
txt  
par  
pid  
st   
490  protected lemma mul_tsum : (∑i, a * f i) = a * (∑i, f i) :=
id                                           
src                                              
typ                                          
doc                                                 
491  if h : ∀i, f i = 0 then by simp [h] else
id   └┘                           
src  └┘                        └────┘ └┘
typ  └┘                     └────┘└┘
doc                             └────┘ └┘
txt                             └────┘ └┘
par                             └────┘ └┘
pid                                  
st                             └────────┘
492  let ⟨i, (hi : f i ≠ 0)⟩ := classical.not_forall.mp h in
id   └─┘                    └──────────────────┘└─┘ 
src  └─┘                       └──────────────────┘└─┘
typ  └─┘                    └──────────────────┘└─┘ 
493  have sum_ne_0 : (∑i, f i) ≠ 0, from ne_of_gt $
id                                 └──────┘
src                                   └──────┘
typ                                └──────┘
doc                    
494    calc 0 < f i : lt_of_le_of_ne (zero_le _) hi.symm
id                   └────────────┘  └─────┘      └───┘
src                   └────────────┘  └─────┘      └───┘
typ                  └────────────┘  └─────┘      └───┘
495      ... ≤ (∑i, f i) : ennreal.le_tsum _,
id                    └─────────────┘
src                      └─────────────┘
typ                   └─────────────┘
doc              
496  have tendsto (λs:finset α, s.sum ((*) a ∘ f)) at_top (𝓝 (a * (∑i, f i))),
id        └─────┘     └────┘   └──┘          └────┘         
src       └─────┘     └────┘     └──┘            └────┘         
typ       └─────┘     └────┘   └──┘          └────┘         
doc       └─────┘     └────┘                       └────┘          
497    by rw [← show (*) a ∘ (λs:finset α, s.sum f) = λs, s.sum ((*) a ∘ f),
id                              └────┘    └──┘                      
src       └────┘     └─┘   └┘└────┘ └┘ └──┘ └┘ └─┘      └─┘   └──
typ       └────┘     └─┘   └┘└────┘└┘ └──┘ └┘ └─┘      └─┘ └──
doc       └────┘     └─┘    └┘└────┘ └┘      └┘  └─┘       └─┘   └──
txt       └────┘     └─┘    └┘       └┘      └┘  └─┘       └─┘   └──
par       └────┘     └─┘    └┘       └┘      └┘  └─┘       └─┘   └──
pid         └──┘     └─┘    └┘       └┘      └┘  └─┘       └─┘   └──
st       └───────────────────────────────────────────────────────────────────
498           from funext $ λ s, finset.mul_sum];
id                 └────┘        └────────────┘
src  ─────────────┘└────┘  └──┘└────────────┘
typ  ─────────────┘└────┘  └──┘└────────────┘
doc  ─────────────┘        └──┘              
txt  ─────────────┘        └──┘              
par  ─────────────┘        └──┘              
pid  ─────────────┘        └──┘              
st   ─────────────────────────────────────────┘└─
499    exact ennreal.tendsto.const_mul (has_sum_tsum ennreal.summable) (or.inl sum_ne_0),
id           └───────────────────────┘  └──────────┘ └──────────────┘   └────┘ └──────┘
src    └────┘└───────────────────────┘ └──────────┘└──────────────┘└┘ └────┘        
typ    └────┘└───────────────────────┘ └──────────┘└──────────────┘└┘ └────┘└──────┘
doc    └────┘                                                      └┘               
txt    └────┘                                                      └┘               
par    └────┘                                                      └┘               
pid                                                               └┘               
st   ──────────────────────────────────────────────────────────────────────────────────┘
500  tsum_eq_has_sum this
id   └─────────────┘ └──┘
src  └─────────────┘
typ  └─────────────┘ └──┘
501  
502  protected lemma tsum_mul : (∑i, f i * a) = (∑i, f i) * a :=
id                                            
src                                                 
typ                                           
doc                                             
503  by simp [mul_comm, ennreal.mul_tsum]
id            └──────┘  └──────────────┘
src     └────┘└──────┘└┘└──────────────┘└─
typ     └────┘└──────┘└┘└──────────────┘└─
doc     └────┘        └┘                └─
txt     └────┘        └┘                └─
par     └────┘        └┘                └─
pid                 └┘                
st     └──────────────────────────────────
504  
src  
typ  
doc  
txt  
par  
pid  
st   
505  @[simp] lemma tsum_supr_eq {α : Type*} (a : α) {f : α → ennreal} :
id                                                         └─────┘
src                                                          └─────┘
typ                                                        └─────┘
doc    └──┘                                                  └─────┘
506    (∑b:α, ⨆ (h : a = b), f b) = f a :=
id                        
src                          
typ                       
doc                     
507  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
508    (by rw [ennreal.tsum_eq_supr_sum]; exact supr_le (assume s,
id             └──────────────────────┘         └─────┘
src        └──┘└──────────────────────┘  └────┘└─────┘       └───
typ        └──┘└──────────────────────┘  └────┘└─────┘       └───
doc        └──┘                          └────┘              └───
txt        └──┘                          └────┘              └───
par        └──┘                          └────┘              └───
pid          └┘                                             └───
st        └───────────────────────────┘└──────────────────────────
509      calc s.sum (λb, ⨆ (h : a = b), f b) ≤ (finset.singleton a).sum (λb, ⨆ (h : a = b), f b) :
id             └──┘                          └──────────────┘
src  ───┘     └──┘  └─┘└────┘    └┘  └──────────────┘ └────┘  └─┘ └────┘      └───
typ  ───┘     └──┘  └─┘└────┘    └┘  └──────────────┘ └────┘  └─┘ └────┘      └───
doc  ───┘           └─┘└────┘     └┘  └──────────────┘ └────┘  └─┘ └────┘      └───
txt  ───┘           └─┘ └────┘      └┘                   └────┘  └─┘ └────┘      └───
par  ───┘           └─┘ └────┘      └┘                   └────┘  └─┘ └────┘      └───
pid  ───┘           └─┘ └────┘      └┘                   └────┘  └─┘ └────┘      └───
st   ──────────────────────────────────────────────────────────────────────────────────────────────
510          finset.sum_le_sum_of_ne_zero $ assume b _ hb,
id           └──────────────────────────┘
src  ───────┘└──────────────────────────┘       └────────
typ  ───────┘└──────────────────────────┘       └────────
doc  ───────┘                                   └────────
txt  ───────┘                                   └────────
par  ───────┘                                   └────────
pid  ───────┘                                   └────────
st   ──────────────────────────────────────────────────────
511            suffices a = b, by simpa using this.symm,
id                                            └───────┘
src  ─────────┘        └─┘  └───┘└──────────┘└───────┘└─
typ  ─────────┘        └─┘  └───┘└──────────┘└───────┘└─
doc  ─────────┘        └─┘  └───┘└──────────┘         └─
txt  ─────────┘        └─┘  └───┘└──────────┘         └─
par  ─────────┘        └─┘  └───┘└──────────┘         └─
pid  ─────────┘        └─┘  └───────────────┘         └─
st   ───────────────────────────┘└────────────────────┘└─
512            classical.by_contradiction $ assume h,
id             └────────────────────────┘
src  ─────────┘└────────────────────────┘       └───
typ  ─────────┘└────────────────────────┘       └───
doc  ─────────┘                                 └───
txt  ─────────┘                                 └───
par  ─────────┘                                 └───
pid  ─────────┘                                 └───
st   ─────────────────────────────────────────────────
513              by simpa [h] using hb
id                                 └┘
src  ───────────┘  └─────┘ └──────┘  
typ  ───────────┘  └─────┘└──────┘└┘
doc  ───────────┘  └─────┘ └──────┘  
txt  ───────────┘  └─────┘ └──────┘  
par  ───────────┘  └─────┘ └──────┘  
pid  ───────────┘  └──────┘ └──────┘  
st   ─────────────┘└───────────────────
514        ... = f a : by simp))
id               
src  ─────┘└──┘   └─┘  └──┘
typ  ─────┘└──┘  └─┘  └──┘
doc  ─────┘└──┘   └─┘  └──┘
txt  ─────┘└──┘   └─┘  └──┘
par  ─────┘└──┘   └─┘  └──┘
pid  ─────────┘   └─┘  └────┘
st   ─────┘└────────────┘└───┘
515    (calc f a ≤ (⨆ (h : a = a), f a) : le_supr (λh:a=a, f a) rfl
id                               └─────┘          └─┘
src                                    └─────┘              └─┘
typ                              └─────┘          └─┘
doc                             
516      ... ≤ (∑b:α, ⨆ (h : a = b), f b) : ennreal.le_tsum _)
id                                └─────────────┘
src                                    └─────────────┘
typ                               └─────────────┘
doc                             
517  
518  lemma has_sum_iff_tendsto_nat {f : ℕ → ennreal} (r : ennreal) :
id                                         └─────┘       └─────┘
src                                        └─────┘       └─────┘
typ                                        └─────┘       └─────┘
doc                                         └─────┘       └─────┘
519    has_sum f r ↔ tendsto (λn:ℕ, (finset.range n).sum f) at_top (𝓝 r) :=
id     └─────┘    └─────┘        └──────────┘  └─┘    └────┘   
src    └─────┘      └─────┘        └──────────┘   └─┘     └────┘  
typ    └─────┘    └─────┘        └──────────┘  └─┘    └────┘   
doc    └─────┘       └─────┘         └──────────┘           └────┘  
520  begin
st   └─────
521    refine ⟨tendsto_sum_nat_of_has_sum, assume h, _⟩,
id             └────────────────────────┘
src    └─────┘ └────────────────────────┘└┘      └────┘
typ    └─────┘ └────────────────────────┘└┘      └────┘
doc    └─────┘ └────────────────────────┘└┘      └────┘
txt    └─────┘                           └┘      └────┘
par    └─────┘                           └┘      └────┘
pid                                     └┘      └────┘
st   ─────────────────────────────────────────────────┘└─
522    rw [← supr_eq_of_tendsto _ h, ← ennreal.tsum_eq_supr_nat],
id           └────────────────┘       └──────────────────────┘
src    └────┘└────────────────┘└─┘ └──┘└──────────────────────┘
typ    └────┘└────────────────┘└─┘└──┘└──────────────────────┘
doc    └────┘                  └─┘ └──┘                        
txt    └────┘                  └─┘ └──┘                        
par    └────┘                  └─┘ └──┘                        
pid      └──┘                  └─┘ └──┘                        
st   ─────────────────────────────┘└──────────────────────────┘└──
523    { exact has_sum_tsum ennreal.summable },
id             └──────────┘ └──────────────┘
src      └────┘└──────────┘└──────────────┘
typ      └────┘└──────────┘└──────────────┘
doc      └────┘                            
txt      └────┘                            
par      └────┘                            
pid                                       
st   ───┘└──────────────────────────────────┘└┘
524    { exact assume s t hst, finset.sum_le_sum_of_subset (finset.range_subset.2 hst) }
id                             └─────────────────────────┘  └─────────────────┘
src      └────┘      └────────┘└─────────────────────────┘ └─────────────────┘└─┘   └┘
typ      └────┘      └────────┘└─────────────────────────┘ └─────────────────┘└─┘   └┘
doc      └────┘      └────────┘                                               └─┘   └┘
txt      └────┘      └────────┘                                               └─┘   └┘
par      └────┘      └────────┘                                               └─┘   └┘
pid                 └────────┘                                               └─┘   
st   ─────────────────────────────────────────────────────────────────────────────────┘└─
525  end
st   ──┘
526  
527  end tsum
528  
529  end ennreal
530  
531  namespace nnreal
532  
533  lemma exists_le_has_sum_of_le {f g : β → nnreal} {r : nnreal}
id                                           └────┘       └────┘
src                                           └────┘       └────┘
typ                                          └────┘       └────┘
doc                                           └────┘       └────┘
534    (hgf : ∀b, g b ≤ f b) (hfr : has_sum f r) : ∃p≤r, has_sum g p :=
id                            └─────┘        └─────┘  
src                                └─────┘            └─────┘
typ                           └─────┘        └─────┘  
doc                                 └─────┘              └─────┘
535  have (∑b, (g b : ennreal)) ≤ r,
id               └─────┘    
src                 └─────┘   
typ              └─────┘    
doc                 └─────┘
536  begin
st   └─────
537    refine has_sum_le (assume b, _) (has_sum_tsum ennreal.summable) (ennreal.has_sum_coe.2 hfr),
id            └────────┘                └──────────┘ └──────────────┘   └─────────────────┘   └─┘
src    └─────┘└────────┘       └─────┘ └──────────┘└──────────────┘└┘ └─────────────────┘└─┘   
typ    └─────┘└────────┘       └─────┘ └──────────┘└──────────────┘└┘ └─────────────────┘└─┘└─┘
doc    └─────┘                 └─────┘                             └┘                    └─┘   
txt    └─────┘                 └─────┘                             └┘                    └─┘   
par    └─────┘                 └─────┘                             └┘                    └─┘   
pid                           └─────┘                             └┘                    └─┘   
st   ────────────────────────────────────────────────────────────────────────────────────────────┘└─
538    exact ennreal.coe_le_coe.2 (hgf _)
id           └────────────────┘    └─┘
src    └────┘└────────────────┘└─┘    └──┘
typ    └────┘└────────────────┘└─┘ └─┘└──┘
doc    └────┘                  └─┘    └──┘
txt    └────┘                  └─┘    └──┘
par    └────┘                  └─┘    └──┘
pid                           └─┘    └─┘
st   ────────────────────────────────────┘
539  end,
st   └─┘
540  let ⟨p, eq, hpr⟩ := ennreal.le_coe_iff.1 this in
id   └─┘    └┘  └─┘     └────────────────┘  └──┘
src          └┘          └────────────────┘
typ  └─┘    └┘  └─┘     └────────────────┘  └──┘
541  ⟨p, hpr, ennreal.has_sum_coe.1 $ eq ▸ has_sum_tsum ennreal.summable⟩
id            └─────────────────┘        └──────────┘ └──────────────┘
src           └─────────────────┘        └──────────┘ └──────────────┘
typ           └─────────────────┘        └──────────┘ └──────────────┘
542  
543  lemma summable_of_le {f g : β → nnreal} (hgf : ∀b, g b ≤ f b) : summable f → summable g
id                                  └────┘                    └──────┘   └──────┘ 
src                                  └────┘                         └──────┘     └──────┘
typ                                 └────┘                    └──────┘   └──────┘ 
doc                                  └────┘                          └──────┘     └──────┘
544  | ⟨r, hfr⟩ := let ⟨p, _, hp⟩ := exists_le_has_sum_of_le hgf hfr in summable_spec hp
id         └─┘     └─┘        └┘     └─────────────────────┘ └─┘        └───────────┘
src                                  └─────────────────────┘            └───────────┘
typ        └─┘     └─┘        └┘     └─────────────────────┘ └─┘        └───────────┘
545  
546  lemma has_sum_iff_tendsto_nat {f : ℕ → nnreal} (r : nnreal) :
id                                         └────┘       └────┘
src                                        └────┘       └────┘
typ                                        └────┘       └────┘
doc                                         └────┘       └────┘
547    has_sum f r ↔ tendsto (λn:ℕ, (finset.range n).sum f) at_top (𝓝 r) :=
id     └─────┘    └─────┘        └──────────┘  └─┘    └────┘   
src    └─────┘      └─────┘        └──────────┘   └─┘     └────┘  
typ    └─────┘    └─────┘        └──────────┘  └─┘    └────┘   
doc    └─────┘       └─────┘         └──────────┘           └────┘  
548  begin
st   └─────
549    rw [← ennreal.has_sum_coe, ennreal.has_sum_iff_tendsto_nat],
id           └─────────────────┘  └─────────────────────────────┘
src    └────┘└─────────────────┘└┘└─────────────────────────────┘
typ    └────┘└─────────────────┘└┘└─────────────────────────────┘
doc    └────┘                   └┘                               
txt    └────┘                   └┘                               
par    └────┘                   └┘                               
pid      └──┘                   └┘                               
st   ──────────────────────────┘└───────────────────────────────┘└──
550    simp only [ennreal.coe_finset_sum.symm],
src    └─────────┘                           
typ    └─────────┘└─────────────────────────┘
doc    └─────────┘                           
txt    └─────────┘                           
par    └─────────┘                           
pid        └──┘└┘                           
st   ────────────────────────────────────────┘└─
551    exact ennreal.tendsto_coe
id           └─────────────────┘
src    └────┘└─────────────────┘
typ    └────┘└─────────────────┘
doc    └────┘                   
txt    └────┘                   
par    └────┘                   
pid                            
st   ───────────────────────────┘
552  end
st   └─┘
553  
554  end nnreal
555  
556  lemma summable_of_nonneg_of_le {f g : β → ℝ}
id                                            
src                                            
typ                                           
557    (hg : ∀b, 0 ≤ g b) (hgf : ∀b, g b ≤ f b) (hf : summable f) : summable g :=
id                                          └──────┘     └──────┘ 
src                                                 └──────┘      └──────┘
typ                                         └──────┘     └──────┘ 
doc                                                   └──────┘      └──────┘
558  let f' (b : β) : nnreal := ⟨f b, le_trans (hg b) (hgf b)⟩ in
id                   └────┘        └──────┘  └┘    └─┘ 
src                   └────┘          └──────┘
typ                  └────┘        └──────┘  └┘    └─┘ 
doc                   └────┘
559  let g' (b : β) : nnreal := ⟨g b, hg b⟩ in
id                   └────┘        └┘ 
src                   └────┘
typ                  └────┘        └┘ 
doc                   └────┘
560  have summable f', from nnreal.summable_coe.1 hf,
id        └──────┘ └┘       └─────────────────┘  └┘
src       └──────┘          └─────────────────┘
typ       └──────┘ └┘       └─────────────────┘  └┘
doc       └──────┘
561  have summable g', from
id        └──────┘ └┘
src       └──────┘
typ       └──────┘ └┘
doc       └──────┘
562    nnreal.summable_of_le (assume b, (@nnreal.coe_le (g' b) (f' b)).2 $ hgf b) this,
id     └───────────────────┘             └───────────┘  └┘    └┘       └─┘   └──┘
src    └───────────────────┘              └───────────┘               
typ    └───────────────────┘             └───────────┘  └┘    └┘       └─┘   └──┘
563  show summable (λb, g' b : β → ℝ), from nnreal.summable_coe.2 this
id        └──────┘     └┘               └─────────────────┘  └──┘
src       └──────┘                         └─────────────────┘
typ       └──────┘     └┘               └─────────────────┘  └──┘
doc       └──────┘
564  
565  lemma has_sum_iff_tendsto_nat_of_nonneg {f : ℕ → ℝ} (hf : ∀i, 0 ≤ f i) (r : ℝ) :
id                                                                         
src                                                                           
typ                                                                        
566    has_sum f r ↔ tendsto (λn:ℕ, (finset.range n).sum f) at_top (𝓝 r) :=
id     └─────┘    └─────┘        └──────────┘  └─┘    └────┘   
src    └─────┘      └─────┘        └──────────┘   └─┘     └────┘  
typ    └─────┘    └─────┘        └──────────┘  └─┘    └────┘   
doc    └─────┘       └─────┘         └──────────┘           └────┘  
567  ⟨tendsto_sum_nat_of_has_sum,
id    └────────────────────────┘
src   └────────────────────────┘
typ   └────────────────────────┘
doc   └────────────────────────┘
568    assume hfr,
id            └─┘
typ           └─┘
569    have 0 ≤ r := ge_of_tendsto at_top_ne_bot hfr $ univ_mem_sets' $ assume i,
id                 └───────────┘ └───────────┘ └─┘   └────────────┘          
src                 └───────────┘ └───────────┘       └────────────┘
typ                └───────────┘ └───────────┘ └─┘   └────────────┘          
570      show 0 ≤ (finset.range i).sum f, from finset.sum_nonneg $ assume i _, hf i,
id                └──────────┘  └─┘         └───────────────┘             └┘ 
src               └──────────┘   └─┘          └───────────────┘
typ               └──────────┘  └─┘         └───────────────┘             └┘ 
doc                └──────────┘
571    let f' (n : ℕ) : nnreal := ⟨f n, hf n⟩, r' : nnreal := ⟨r, this⟩ in
id                     └────┘        └┘         └────┘       └──┘
src                    └────┘                      └────┘
typ                    └────┘        └┘         └────┘       └──┘
doc                     └────┘                      └────┘
572    have f_eq : f = (λi:ℕ, (f' i : ℝ)) := rfl,
id                          └┘          └─┘
src                                       └─┘
typ                         └┘          └─┘
573    have r_eq : r = r' := rfl,
id                   └┘    └─┘
src                         └─┘
typ                  └┘    └─┘
574    begin
st     └─────
575      rw [f_eq, r_eq, nnreal.has_sum_coe, nnreal.has_sum_iff_tendsto_nat, ← nnreal.tendsto_coe],
id           └──┘  └──┘  └────────────────┘  └────────────────────────────┘    └────────────────┘
src      └──┘    └┘    └┘└────────────────┘└┘└────────────────────────────┘└──┘└────────────────┘
typ      └──┘└──┘└┘└──┘└┘└────────────────┘└┘└────────────────────────────┘└──┘└────────────────┘
doc      └──┘    └┘    └┘                  └┘                              └──┘                  
txt      └──┘    └┘    └┘                  └┘                              └──┘                  
par      └──┘    └┘    └┘                  └┘                              └──┘                  
pid        └┘    └┘    └┘                  └┘                              └──┘                  
st   ───────────┘└────┘└──────────────────┘└──────────────────────────────┘└────────────────────┘└──
576      simp only [nnreal.coe_sum],
id                  └────────────┘
src      └─────────┘└────────────┘
typ      └─────────┘└────────────┘
doc      └─────────┘              
txt      └─────────┘              
par      └─────────┘              
pid          └──┘└┘              
st   ─────────────────────────────┘└─
577      exact hfr
id             └─┘
src      └────┘   
typ      └────┘└─┘
doc      └────┘   
txt      └────┘   
par      └────┘   
pid              
st   ──────────────
578    end⟩
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
579  
580  lemma infi_real_pos_eq_infi_nnreal_pos {α : Type*} [complete_lattice α] {f : ℝ → α} :
id                                                       └──────────────┘           
src                                                      └──────────────┘         
typ                                                      └──────────────┘           
doc                                                      └──────────────┘
581    (⨅(n:ℝ) (h : n > 0), f n) = (⨅(n:nnreal) (h : n > 0), f n) :=
id                             └────┘             
src                               └────┘            
typ                            └────┘             
doc                                  └────┘             
582  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
583    (le_infi $ assume n, le_infi $ assume hn, infi_le_of_le n $ infi_le _ (nnreal.coe_pos.2 hn))
id      └─────┘            └─────┘          └┘  └───────────┘    └─────┘    └────────────┘  └┘
src     └─────┘             └─────┘              └───────────┘     └─────┘    └────────────┘
typ     └─────┘            └─────┘          └┘  └───────────┘    └─────┘    └────────────┘  └┘
584    (le_infi $ assume r, le_infi $ assume hr, infi_le_of_le ⟨r, le_of_lt hr⟩ $ infi_le _ hr)
id      └─────┘            └─────┘          └┘  └───────────┘    └──────┘ └┘    └─────┘   └┘
src     └─────┘             └─────┘              └───────────┘     └──────┘       └─────┘
typ     └─────┘            └─────┘          └┘  └───────────┘    └──────┘ └┘    └─────┘   └┘
585  
586  section
587  variables [emetric_space β]
id              └───────────┘
src             └───────────┘
typ             └───────────┘
doc             └───────────┘
588  open lattice ennreal filter emetric
589  
590  /-- In an emetric ball, the distance between points is everywhere finite -/
591  lemma edist_ne_top_of_mem_ball {a : β} {r : ennreal} (x y : ball a r) : edist x.1 y.1 ≠ ⊤ :=
id                                              └─────┘         └──┘      └───┘      
src                                              └─────┘         └──┘        └───┘        
typ                                             └─────┘         └──┘      └───┘      
doc                                              └─────┘         └──┘
592  lt_top_iff_ne_top.1 $
id   └───────────────┘
src  └───────────────┘
typ  └───────────────┘
593  calc edist x y ≤ edist a x + edist a y : edist_triangle_left x.1 y.1 a
id        └───┘     └───┘    └───┘     └─────────────────┘     
src       └───┘       └───┘      └───┘       └─────────────────┘     
typ       └───┘     └───┘    └───┘     └─────────────────┘     
doc                                           └─────────────────┘
594    ... < r + r : by rw [edist_comm a x, edist_comm a y]; exact add_lt_add x.2 y.2
id                       └────────┘    └────────┘           └────────┘    
src                    └──┘└────────┘  └┘└────────┘    └────┘└────────┘ └─┘ └──
typ                  └──┘└────────┘└┘└────────┘  └────┘└────────┘└─┘└──
doc                     └──┘            └┘              └────┘           └─┘ └──
txt                     └──┘            └┘              └────┘           └─┘ └──
par                     └──┘            └┘              └────┘           └─┘ └──
pid                       └┘            └┘                              └─┘ └──
st                     └─────────────────┘└──────────────┘└──────────────────────────
595    ... ≤ ⊤ : le_top
id              └────┘
src  ─┘         └────┘
typ  ─┘         └────┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
596  
597  /-- Each ball in an extended metric space gives us a metric space, as the edist
598  is everywhere finite. -/
599  def metric_space_emetric_ball (a : β) (r : ennreal) : metric_space (ball a r) :=
id                                             └─────┘    └──────────┘  └──┘  
src                                             └─────┘    └──────────┘  └──┘
typ                                            └─────┘    └──────────┘  └──┘  
doc                                             └─────┘    └──────────┘  └──┘
600  emetric_space.to_metric_space edist_ne_top_of_mem_ball
id   └───────────────────────────┘ └──────────────────────┘
src  └───────────────────────────┘ └──────────────────────┘
typ  └───────────────────────────┘ └──────────────────────┘
doc  └───────────────────────────┘ └──────────────────────┘
601  
602  local attribute [instance] metric_space_emetric_ball
id                              └───────────────────────┘
src                             └───────────────────────┘
typ                             └───────────────────────┘
doc                             └───────────────────────┘
603  
604  lemma nhds_eq_nhds_emetric_ball (a x : β) (r : ennreal) (h : x ∈ ball a r) :
id                                                 └─────┘         └──┘  
src                                                 └─────┘          └──┘
typ                                                └─────┘         └──┘  
doc                                                 └─────┘           └──┘
605    𝓝 x = map (coe : ball a r → β) (𝓝 ⟨x, h⟩) :=
id        └─┘  └─┘   └──┘            
src        └─┘  └─┘   └──┘           
typ       └─┘  └─┘   └──┘            
doc         └─┘        └──┘           
606  (map_nhds_subtype_val_eq _ $ mem_nhds_sets emetric.is_open_ball h).symm
id    └─────────────────────┘     └───────────┘ └──────────────────┘  └──┘
src   └─────────────────────┘     └───────────┘ └──────────────────┘   └──┘
typ   └─────────────────────┘     └───────────┘ └──────────────────┘  └──┘
607  end
608  
609  section
610  variable [emetric_space α]
id             └───────────┘
src            └───────────┘
typ            └───────────┘
doc            └───────────┘
611  open emetric
612  
613  /-- Yet another metric characterization of Cauchy sequences on integers. This one is often the
614  most efficient. -/
615  lemma emetric.cauchy_seq_iff_le_tendsto_0 [inhabited β] [semilattice_sup β] {s : β → α} :
id                                              └───────┘    └─────────────┘           
src                                             └───────┘     └─────────────┘
typ                                             └───────┘    └─────────────┘           
doc                                                           └─────────────┘
616    cauchy_seq s ↔ (∃ (b: β → ennreal), (∀ n m N : β, N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N)
id     └────────┘           └─────┘                         └───┘           
src    └────────┘              └─────┘                              └───┘             
typ    └────────┘           └─────┘                         └───┘           
doc    └────────┘                └─────┘
617                      ∧ (tendsto b at_top (𝓝 0))) :=
id                         └─────┘  └────┘  
src                        └─────┘   └────┘  
typ                        └─────┘  └────┘  
doc                         └─────┘   └────┘  
618  ⟨begin
st    └─────
619    assume hs,
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
pid    └───────┘
st   ──────────┘└─
620    rw emetric.cauchy_seq_iff at hs,
id        └────────────────────┘
src    └─┘└────────────────────┘└────┘
typ    └─┘└────────────────────┘└────┘
doc    └─┘└────────────────────┘└────┘
txt    └─┘                      └────┘
par    └─┘                      └────┘
pid                            └────┘
st   ────────────────────────────────┘└─
621    /- `s` is Cauchy sequence. The sequence `b` will be constructed by taking
st   ────────────────────────────────────────────────────────────────────────────
622    the supremum of the distances between `s n` and `s m` for `n m ≥ N`-/
st   ────────────────────────────────────────────────────────────────────────
623    let b := λN, Sup ((λ(p : β × β), edist (s p.1) (s p.2))''{p | p.1 ≥ N ∧ p.2 ≥ N}),
id                  └─┘               └───┘                └┘        
src    └───────┘ └─┘└─┘   └───┘  └─┘└───┘   └──┘   └──┘└┘└──┘ └─┘   └─┘  └┘
typ    └───────┘ └─┘└─┘   └───┘ └─┘└───┘   └──┘  └──┘└┘└──┘ └─┘   └─┘  └┘
doc    └───────┘ └─┘└─┘   └───┘   └─┘        └──┘   └──┘   └──┘ └─┘    └─┘  └┘
txt    └───────┘ └─┘      └───┘   └─┘        └──┘   └──┘   └──┘ └─┘    └─┘  └┘
par    └───────┘ └─┘      └───┘   └─┘        └──┘   └──┘   └──┘ └─┘    └─┘  └┘
pid    └───┘└─┘ └─┘      └───┘   └─┘        └──┘   └──┘   └──┘ └─┘    └─┘  └┘
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
624    --Prove that it bounds the distances of points in the Cauchy sequence
st   ────────────────────────────────────────────────────────────────────────
625    have C : ∀ n m N, N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N,
id                                     └───┘              
src    └───────┘ └────┘        └───┘   └┘   └┘  
typ    └───────┘ └────┘       └───┘   └┘  └┘ 
doc    └───────┘ └────┘                 └┘   └┘  
txt    └───────┘ └────┘                 └┘   └┘  
par    └───────┘ └────┘                 └┘   └┘  
pid    └────┘└─┘ └────┘                 └┘   └┘  
st   ──────────────────────────────────────────────────────────┘└─
626    { refine λm n N hm hn, le_Sup _,
id                            └────┘
src      └─────┘ └───────────┘└────┘└┘
typ      └─────┘ └───────────┘└────┘└┘
doc      └─────┘ └───────────┘      └┘
txt      └─────┘ └───────────┘      └┘
par      └─────┘ └───────────┘      └┘
pid             └───────────┘      └┘
st   ───┘└───────────────────────────┘└─
627      use (prod.mk m n),
id            └─────┘  
src      └──┘ └─────┘  
typ      └──┘ └─────┘
doc      └──┘          
txt      └──┘          
par      └──┘          
pid                   
st   ────────────────────┘└─
628      simp only [and_true, eq_self_iff_true, set.mem_set_of_eq],
id                  └──────┘  └──────────────┘  └───────────────┘
src      └─────────┘└──────┘└┘└──────────────┘└┘└───────────────┘
typ      └─────────┘└──────┘└┘└──────────────┘└┘└───────────────┘
doc      └─────────┘        └┘                └┘                 
txt      └─────────┘        └┘                └┘                 
par      └─────────┘        └┘                └┘                 
pid          └──┘└┘        └┘                └┘                 
st   ────────────────────────────────────────────────────────────┘└─
629      exact ⟨hm, hn⟩ },
id              └┘  └┘
src      └────┘   └┘  └┘
typ      └────┘ └┘└┘└┘└┘
doc      └────┘   └┘  └┘
txt      └────┘   └┘  └┘
par      └────┘   └┘  └┘
pid              └┘  
st   ──────────────────┘└┘
630    --Prove that it tends to `0`, by using the Cauchy property of `s`
st   ────────────────────────────────────────────────────────────────────
631    have D : tendsto b at_top (𝓝 0),
id              └─────┘  └────┘  
src    └───────┘└─────┘ └────┘ └─┘
typ    └───────┘└─────┘└────┘ └─┘
doc    └───────┘└─────┘ └────┘ └─┘
txt    └───────┘                └─┘
par    └───────┘                └─┘
pid    └────┘└─┘                └─┘
st   ────────────────────────────────┘└─
632    { refine tendsto_order.2 ⟨λa ha, absurd ha (ennreal.not_lt_zero), λε εpos, _⟩,
id              └───────────┘           └────┘     └─────────────────┘
src      └─────┘└───────────┘└─┘  └────┘└────┘   └─────────────────┘└─┘ └────────┘
typ      └─────┘└───────────┘└─┘  └────┘└────┘   └─────────────────┘└─┘ └────────┘
doc      └─────┘             └─┘  └────┘                            └─┘ └────────┘
txt      └─────┘             └─┘  └────┘                            └─┘ └────────┘
par      └─────┘             └─┘  └────┘                            └─┘ └────────┘
pid                         └─┘  └────┘                            └─┘ └────────┘
st   ───┘└─────────────────────────────────────────────────────────────────────────┘└─
633      rcases dense εpos with ⟨δ, δpos, δlt⟩,
id              └───┘ └──┘
src      └─────┘└───┘    └──────────────────┘
typ      └─────┘└───┘└──┘└──────────────────┘
doc      └─────┘         └──────────────────┘
txt      └─────┘         └──────────────────┘
par      └─────┘         └──────────────────┘
pid                     └──────────────────┘
st   ────────────────────────────────────────┘└─
634      rcases hs δ δpos with ⟨N, hN⟩,
id              └┘  └──┘
src      └─────┘       └───────────┘
typ      └─────┘└┘└──┘└───────────┘
doc      └─────┘       └───────────┘
txt      └─────┘       └───────────┘
par      └─────┘       └───────────┘
pid                   └───────────┘
st   ────────────────────────────────┘└─
635      refine filter.mem_at_top_sets.2 ⟨N, λn hn, _⟩,
id              └────────────────────┘    
src      └─────┘└────────────────────┘└─┘  └┘ └──────┘
typ      └─────┘└────────────────────┘└─┘ └┘ └──────┘
doc      └─────┘                      └─┘  └┘ └──────┘
txt      └─────┘                      └─┘  └┘ └──────┘
par      └─────┘                      └─┘  └┘ └──────┘
pid                                  └─┘  └┘ └──────┘
st   ────────────────────────────────────────────────┘└─
636      have : b n ≤ δ := Sup_le begin
id                      └────┘
src      └─────┘    └──┘└────┘     
typ      └─────┘ └──┘└────┘     
doc      └─────┘    └──┘           
txt      └─────┘    └──┘           
par      └─────┘    └──┘           
pid      └───┘└┘    └──┘           
st   ────────────────────────────┘└─────
637        simp only [and_imp, set.mem_image, set.mem_set_of_eq, exists_imp_distrib, prod.exists],
id                    └─────┘  └───────────┘  └───────────────┘  └────────────────┘  └─────────┘
src  ─────┘└─────────┘└─────┘└┘└───────────┘└┘└───────────────┘└┘└────────────────┘└┘└─────────┘└─
typ  ─────┘└─────────┘└─────┘└┘└───────────┘└┘└───────────────┘└┘└────────────────┘└┘└─────────┘└─
doc  ─────┘└─────────┘       └┘             └┘                 └┘                  └┘           └─
txt  ─────┘└─────────┘       └┘             └┘                 └┘                  └┘           └─
par  ─────┘└─────────┘       └┘             └┘                 └┘                  └┘           └─
pid  ────────────────┘       └┘             └┘                 └┘                  └┘           └──
st   ───────────────────────────────────────────────────────────────────────────────────────────┘└─
638        intros d p q hp hq hd,
src  ─────┘└───────────────────┘└─
typ  ─────┘└───────────────────┘└─
doc  ─────┘└───────────────────┘└─
txt  ─────┘└───────────────────┘└─
par  ─────┘└───────────────────┘└─
pid  ─────────────────────────────
st   ──────────────────────────┘└─
639        rw ← hd,
id              └┘
src  ─────┘└───┘  └─
typ  ─────┘└───┘└┘└─
doc  ─────┘└───┘  └─
txt  ─────┘└───┘  └─
par  ─────┘└───┘  └─
pid  ──────────┘  └─
st   ────────────┘└─
640        exact le_of_lt (hN q p (le_trans hn hq) (le_trans hn hp))
id               └──────┘  └┘                └┘   └──────┘ └┘ └┘
src  ─────┘└────┘└──────┘                  └┘ └──────┘    └──
typ  ─────┘└────┘└──────┘ └┘           └┘└┘ └──────┘└┘└┘└──
doc  ─────┘└────┘                          └┘             └──
txt  ─────┘└────┘                          └┘             └──
par  ─────┘└────┘                          └┘             └──
pid  ───────────┘                          └┘             └──
st   ────────────────────────────────────────────────────────────────
641      end,
src  ───┘└─┘
typ  ───┘└─┘
doc  ───┘└─┘
txt  ───┘└─┘
par  ───┘└─┘
pid  ──────┘
st   ───┘└─┘└─
642      simpa using lt_of_le_of_lt this δlt },
id                   └────────────┘ └──┘ └─┘
src      └──────────┘└────────────┘       
typ      └──────────┘└────────────┘└──┘└─┘
doc      └──────────┘                     
txt      └──────────┘                     
par      └──────────┘                     
pid           └────┘                     
st   ───────────────────────────────────────┘└┘
643    -- Conclude
st   ──────────────
644    exact ⟨b, ⟨C, D⟩⟩
id                 
src    └────┘  └┘  └┘ └─┘
typ    └────┘ └┘ └┘└─┘
doc    └────┘  └┘  └┘ └─┘
txt    └────┘  └┘  └┘ └─┘
par    └────┘  └┘  └┘ └─┘
pid           └┘  └┘ └┘
st   ───────────────────┘
645  end,
st   └─┘
646  begin
st   └─────
647    rintros ⟨b, ⟨b_bound, b_lim⟩⟩,
src    └───────────────────────────┘
typ    └───────────────────────────┘
doc    └───────────────────────────┘
txt    └───────────────────────────┘
par    └───────────────────────────┘
pid           └────────────────────┘
st   ──────────────────────────────┘└─
648    /-b : ℕ → ℝ, b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N,
st   ─────────────────────────────────────────────────────────────────────────────────
649      b_lim : tendsto b at_top (𝓝 0)-/
st   ─────────────────────────────────────
650    refine emetric.cauchy_seq_iff.2 (λε εpos, _),
id            └────────────────────┘
src    └─────┘└────────────────────┘└─┘  └────────┘
typ    └─────┘└────────────────────┘└─┘  └────────┘
doc    └─────┘└────────────────────┘└─┘  └────────┘
txt    └─────┘                      └─┘  └────────┘
par    └─────┘                      └─┘  └────────┘
pid                                └─┘  └────────┘
st   ─────────────────────────────────────────────┘└─
651    have : ∀ᶠ n in at_top, b n < ε := (tendsto_order.1 b_lim ).2 _ εpos,
id            └┘   └┘ └────┘          └───────────┘   └───┘       └──┘
src    └─────┘└┘└─┘└┘└────┘   └──┘ └───────────┘└─┘     └─────┘
typ    └─────┘└┘└─┘└┘└────┘ └──┘ └───────────┘└─┘└───┘└─────┘└──┘
doc    └─────┘└┘└─┘└┘└────┘    └──┘              └─┘     └─────┘
txt    └─────┘  └─┘             └──┘              └─┘     └─────┘
par    └─────┘  └─┘             └──┘              └─┘     └─────┘
pid    └───┘└┘  └─┘             └──┘              └─┘     └─────┘
st   ────────────────────────────────────────────────────────────────────┘└─
652    rcases filter.mem_at_top_sets.1 this with ⟨N, hN⟩,
id            └────────────────────┘   └──┘
src    └─────┘└────────────────────┘└─┘    └───────────┘
typ    └─────┘└────────────────────┘└─┘└──┘└───────────┘
doc    └─────┘                      └─┘    └───────────┘
txt    └─────┘                      └─┘    └───────────┘
par    └─────┘                      └─┘    └───────────┘
pid                                └─┘    └───────────┘
st   ──────────────────────────────────────────────────┘└─
653    exact ⟨N, λm n hm hn, calc
src    └────┘  └┘ └─────────┘    
typ    └────┘  └┘ └─────────┘    
doc    └────┘  └┘ └─────────┘    
txt    └────┘  └┘ └─────────┘    
par    └────┘  └┘ └─────────┘    
pid           └┘ └─────────┘    
st   ─────────────────────────────
654      edist (s n) (s m) ≤ b N : b_bound n m N hn hm
id       └───┘                   └─────┘
src  ───┘└───┘   └┘   └┘   └─┘              
typ  ───┘└───┘   └┘  └┘  └─┘└─────┘       
doc  ───┘        └┘   └┘   └─┘              
txt  ───┘        └┘   └┘   └─┘              
par  ───┘        └┘   └┘   └─┘              
pid  ───┘        └┘   └┘   └─┘              
st   ──────────────────────────────────────────────────
655      ... < ε : (hN _ (le_refl N)) ⟩
id                 └┘    └─────┘ 
src  ───────┘  └─┘   └─┘ └─────┘ └───┘
typ  ───────┘ └─┘ └┘└─┘ └─────┘└───┘
doc  ───────┘  └─┘   └─┘         └───┘
txt  ───────┘  └─┘   └─┘         └───┘
par  ───────┘  └─┘   └─┘         └───┘
pid  ───────┘  └─┘   └─┘         └──┘
st   ──────────────────────────────────┘
656  end⟩
st   └─┘
657  
658  lemma continuous_of_le_add_edist {f : α → ennreal} (C : ennreal)
id                                            └─────┘       └─────┘
src                                            └─────┘       └─────┘
typ                                           └─────┘       └─────┘
doc                                            └─────┘       └─────┘
659    (hC : C ≠ ⊤) (h : ∀x y, f x ≤ f y + C * edist x y) : continuous f :=
id                                └───┘      └────────┘ 
src                                       └───┘        └────────┘
typ                               └───┘      └────────┘ 
doc                                                         └────────┘
660  begin
st   └─────
661    refine continuous_iff_continuous_at.2 (λx, tendsto_order.2 ⟨_, _⟩),
id            └──────────────────────────┘        └───────────┘
src    └─────┘└──────────────────────────┘└─┘  └─┘└───────────┘└─┘ └────┘
typ    └─────┘└──────────────────────────┘└─┘  └─┘└───────────┘└─┘ └────┘
doc    └─────┘                            └─┘  └─┘             └─┘ └────┘
txt    └─────┘                            └─┘  └─┘             └─┘ └────┘
par    └─────┘                            └─┘  └─┘             └─┘ └────┘
pid                                      └─┘  └─┘             └─┘ └────┘
st   ───────────────────────────────────────────────────────────────────┘└─
662    show ∀e, e < f x → ∀ᶠ y in 𝓝 x, e < f y,
id                       └┘   └┘       
src    └───┘      └┘└─┘└┘    
typ    └───┘      └┘└─┘└┘  
doc    └───┘       └┘└─┘└┘    
txt    └───┘         └─┘        
par    └───┘         └─┘        
pid    └───┘         └─┘        
st   ───────────────────────────────────────────
663    { assume e he,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ───┘└─────────┘└─
664      let ε := min (f x - e) 1,
id                └─┘     
src      └───────┘└─┘    └─┘
typ      └───────┘└─┘ └─┘
doc      └───────┘        └─┘
txt      └───────┘        └─┘
par      └───────┘        └─┘
pid      └───┘└─┘        └┘
st   ───────────────────────────┘└─
665      have : ε < ⊤ := lt_of_le_of_lt (min_le_right _ _) (by simp [lt_top_iff_ne_top]),
id                     └────────────┘  └──────────┘                └───────────────┘
src      └─────┘  └──┘└────────────┘ └──────────┘└────┘   └────┘└───────────────┘
typ      └─────┘ └──┘└────────────┘ └──────────┘└────┘   └────┘└───────────────┘
doc      └─────┘   └──┘                           └────┘   └────┘                 
txt      └─────┘   └──┘                           └────┘   └────┘                 
par      └─────┘   └──┘                           └────┘   └────┘                 
pid      └───┘└┘   └──┘                           └────┘   └─────┘                 └┘
st   ────────────────────────────────────────────────────────┘└───────────────────────┘└─
666      have : 0 < ε := by simp [ε, hC, he, ennreal.zero_lt_one],
id                                 └┘  └┘  └─────────────────┘
src      └───────┘  └──┘  └────┘ └┘  └┘  └┘└─────────────────┘
typ      └───────┘ └──┘  └────┘└┘└┘└┘└┘└┘└─────────────────┘
doc      └───────┘  └──┘  └────┘ └┘  └┘  └┘                   
txt      └───────┘  └──┘  └────┘ └┘  └┘  └┘                   
par      └───────┘  └──┘  └────┘ └┘  └┘  └┘                   
pid      └───┘└──┘  └──┘  └─────┘ └┘  └┘  └┘                   
st   ─────────────────────┘└────────────────────────────────────┘└─
667      have : 0 < C⁻¹ * (ε/2) := bot_lt_iff_ne_bot.2 (by simp [hC, (ne_of_lt this).symm, ennreal.mul_eq_zero]),
id                  └┘         └───────────────┘             └┘   └──────┘ └──┘        └─────────────────┘
src      └───────┘  └┘  └────┘└───────────────┘└─┘   └────┘  └┘ └──────┘    └──────┘└─────────────────┘
typ      └───────┘ └┘ └────┘└───────────────┘└─┘   └────┘└┘└┘ └──────┘└──┘└──────┘└─────────────────┘
doc      └───────┘        └────┘                 └─┘   └────┘  └┘             └──────┘                   
txt      └───────┘        └────┘                 └─┘   └────┘  └┘             └──────┘                   
par      └───────┘        └────┘                 └─┘   └────┘  └┘             └──────┘                   
pid      └───┘└──┘        └┘└──┘                 └─┘   └─────┘  └┘             └──────┘                   └┘
st   ────────────────────────────────────────────────────┘└───────────────────────────────────────────────────┘└─
668      have I : C * (C⁻¹ * (ε/2)) < ε,
id                                   
src      └───────┘          └──┘ 
typ      └───────┘         └──┘ 
doc      └───────┘          └──┘ 
txt      └───────┘          └──┘ 
par      └───────┘          └──┘ 
pid      └────┘└─┘          └──┘ 
st   ─────────────────────────────────┘└─
669      { by_cases C_zero : C = 0,
id                            
src        └───────┘      └─┘ └┘
typ        └───────┘      └─┘└┘
doc        └───────┘      └─┘  └┘
txt        └───────┘      └─┘  └┘
par        └───────┘      └─┘  └┘
pid                      └─┘  
st   ─────┘└─────────────────────┘└─
670        { simp [C_zero, ‹0 < ε›] },
id                 └────┘      
src          └────┘      └┘└┘  └┘
typ          └────┘└────┘└┘└┘ └┘
doc          └────┘      └┘└┘  └┘
txt          └────┘      └┘ └┘   └┘
par          └────┘      └┘ └┘   └┘
pid                    └┘ └┘   
st   ───────┘└─────────────────────┘└┘
671        { calc C * (C⁻¹ * (ε/2)) = (C * C⁻¹) * (ε/2) : by simp [mul_assoc]
id           └──┘                                                 └───────┘
src          └──┘                                            └────┘└───────┘└─
typ          └──┘                                           └────┘└───────┘└─
doc          └──┘                                            └────┘         └─
txt                                                          └────┘         └─
par                                                          └────┘         └─
pid                                                                       
st   ──────────────────────────────────────────────────────┘└─────────────────
672          ... = ε/2 : by simp [ennreal.mul_inv_cancel C_zero hC]
id                                └────────────────────┘ └────┘ └┘
src  ───────┘               └────┘└────────────────────┘        └─
typ  ───────┘               └────┘└────────────────────┘└────┘└┘└─
doc  ───────┘               └────┘                              └─
txt  ───────┘               └────┘                              └─
par  ───────┘               └────┘                              └─
pid  ───────┘                                                 
st   ───────┘└────────────┘└────────────────────────────────────────
673          ... < ε : ennreal.half_lt_self (bot_lt_iff_ne_bot.1 ‹0 < ε›) (lt_top_iff_ne_top.1 ‹ε < ⊤›) }},
id                     └──────────────────┘  └───────────────┘            └───────────────┘   
src  ───────┘          └──────────────────┘  └───────────────┘            └───────────────┘
typ  ───────┘          └──────────────────┘  └───────────────┘            └───────────────┘   
doc  ───────┘
txt  ───────┘
par  ───────┘
pid  ───────┘
st   ───────┘└────────────────────────────────────────────────────────────────────────────────────────┘└──┘
674      have : ball x (C⁻¹ * (ε/2)) ⊆ {y : α | e < f y},
id              └──┘                         
src      └─────┘└──┘         └──┘└──┘ └─┘    
typ      └─────┘└──┘      └──┘└──┘└─┘  
doc      └─────┘└──┘         └──┘  └──┘ └─┘    
txt      └─────┘             └──┘  └──┘ └─┘    
par      └─────┘             └──┘  └──┘ └─┘    
pid      └───┘└┘             └──┘  └──┘ └─┘    
st   ──────────────────────────────────────────────────┘└─
675      { rintros y hy,
src        └──────────┘
typ        └──────────┘
doc        └──────────┘
txt        └──────────┘
par        └──────────┘
pid               └───┘
st   ─────┘└──────────┘└─
676        by_cases htop : f y = ⊤,
id                          
src        └───────┘    └─┘   
typ        └───────┘    └─┘ 
doc        └───────┘    └─┘   
txt        └───────┘    └─┘   
par        └───────┘    └─┘   
pid                    └─┘   
st   ────────────────────────────┘└─
677        { simp [htop, lt_top_iff_ne_top, ne_top_of_lt he] },
id                 └──┘  └───────────────┘  └──────────┘ └┘
src          └────┘    └┘└───────────────┘└┘└──────────┘  └┘
typ          └────┘└──┘└┘└───────────────┘└┘└──────────┘└┘└┘
doc          └────┘    └┘                 └┘              └┘
txt          └────┘    └┘                 └┘              └┘
par          └────┘    └┘                 └┘              └┘
pid                  └┘                 └┘              
st   ───────┘└──────────────────────────────────────────────┘└┘
678        { simp at hy,
src          └────────┘
typ          └────────┘
doc          └────────┘
txt          └────────┘
par          └────────┘
pid              └───┘
st   ─────────────────┘└─
679          have : e + ε < f y + ε := calc
id                            
src          └─────┘       └──┘    
typ          └─────┘   └──┘    
doc          └─────┘        └──┘    
txt          └─────┘        └──┘    
par          └─────┘        └──┘    
pid          └───┘└┘        └──┘    
st   ───────────────────────────────────────
680            e + ε ≤ e + (f x - e) : add_le_add_left' (min_le_left _ _)
id                                                     └─────────┘
src  ─────────┘           └──┘                 └─────────┘└─────
typ  ─────────┘         └──┘                 └─────────┘└─────
doc  ─────────┘           └──┘                            └─────
txt  ─────────┘           └──┘                            └─────
par  ─────────┘           └──┘                            └─────
pid  ─────────┘           └──┘                            └─────
st   ─────────────────────────────────────────────────────────────────────
681            ... = f x : by simp [le_of_lt he]
id                                  └──────┘ └┘
src  ─────────────┘   └─┘  └────┘└──────┘  └─
typ  ─────────────┘   └─┘  └────┘└──────┘└┘└─
doc  ─────────────┘   └─┘  └────┘          └─
txt  ─────────────┘   └─┘  └────┘          └─
par  ─────────────┘   └─┘  └────┘          └─
pid  ─────────────┘   └─┘  └─────┘          └─
st   ───────────────────────┘└───────────────────
682            ... ≤ f y + C * edist x y : h x y
id                            └───┘         
src  ─────────┘└──┘      └───┘  └─┘   
typ  ─────────┘└──┘     └───┘  └─┘
doc  ─────────┘└──┘             └─┘   
txt  ─────────┘└──┘             └─┘   
par  ─────────┘└──┘             └─┘   
pid  ─────────────┘             └─┘   
st   ─────────┘└─────────────────────────────────
683            ... = f y + C * edist y x : by simp [edist_comm]
id                                                  └────────┘
src  ─────────────┘             └─┘  └────┘└────────┘└─
typ  ─────────────┘             └─┘  └────┘└────────┘└─
doc  ─────────────┘             └─┘  └────┘          └─
txt  ─────────────┘             └─┘  └────┘          └─
par  ─────────────┘             └─┘  └────┘          └─
pid  ─────────────┘             └─┘  └─────┘          └─
st   ───────────────────────────────────────┘└──────────────────
684            ... ≤ f y + C * (C⁻¹ * (ε/2)) :
src  ─────────┘└──┘              └─────
typ  ─────────┘└──┘              └─────
doc  ─────────┘└──┘              └─────
txt  ─────────┘└──┘              └─────
par  ─────────┘└──┘              └─────
pid  ─────────────┘              └─────
st   ─────────┘└───────────────────────────────
685              add_le_add_left' $ canonically_ordered_semiring.mul_le_mul (le_refl _) (le_of_lt hy)
id               └──────────────┘   └─────────────────────────────────────┘  └─────┘              └┘
src  ───────────┘└──────────────┘ └─────────────────────────────────────┘ └─────┘└──┘           └─
typ  ───────────┘└──────────────┘ └─────────────────────────────────────┘ └─────┘└──┘         └┘└─
doc  ───────────┘                                                                └──┘           └─
txt  ───────────┘                                                                └──┘           └─
par  ───────────┘                                                                └──┘           └─
pid  ───────────┘                                                                └──┘           └─
st   ─────────────────────────────────────────────────────────────────────────────────────────────────
686            ... < f y + ε : (ennreal.add_lt_add_iff_left (lt_top_iff_ne_top.2 htop)).2 I,
id                             └─────────────────────────┘  └───────────────┘   └──┘     
src  ─────────────┘     └─┘ └─────────────────────────┘ └───────────────┘└─┘    └───┘
typ  ─────────────┘    └─┘ └─────────────────────────┘ └───────────────┘└─┘└──┘└───┘
doc  ─────────────┘     └─┘                                              └─┘    └───┘
txt  ─────────────┘     └─┘                                              └─┘    └───┘
par  ─────────────┘     └─┘                                              └─┘    └───┘
pid  ─────────────┘     └─┘                                              └─┘    └───┘
st   ─────────────────────────────────────────────────────────────────────────────────────┘└─
687          show e < f y, from
id                    
src          └───┘      └────
typ          └───┘   └────
doc          └───┘      └────
txt          └───┘      └────
par          └───┘      └────
pid          └───┘      └────
st   ───────────────────┘└──────
688            (ennreal.add_lt_add_iff_right ‹ε < ⊤›).1 this }},
id              └──────────────────────────┘           └──┘
src  ─────────┘ └──────────────────────────┘     └──┘    
typ  ─────────┘ └──────────────────────────┘    └──┘└──┘
doc  ─────────┘                                  └──┘    
txt  ─────────┘                                  └──┘    
par  ─────────┘                                  └──┘    
pid  ─────────┘                                  └──┘    
st   ───────────────────────────────────────────────────────┘└─┘
689      apply filter.mem_sets_of_superset (ball_mem_nhds _ (‹0 < C⁻¹ * (ε/2)›)) this },
id             └─────────────────────────┘  └───────────┘                      └──┘
src      └────┘└─────────────────────────┘ └───────────┘└─┘  └┘        └┘ └─┘    
typ      └────┘└─────────────────────────┘ └───────────┘└─┘  └┘      └┘ └─┘└──┘
doc      └────┘                                         └─┘  └┘        └┘ └─┘    
txt      └────┘                                         └─┘  └┘        └┘ └─┘    
par      └────┘                                         └─┘  └┘        └┘ └─┘    
pid                                                    └─┘  └┘        └┘ └─┘    
st   ────────────────────────────────────────────────────────────────────────────────┘└┘
690    show ∀e, f x < e → ∀ᶠ y in 𝓝 x, f y < e,
id                       └┘   └┘    
src    └───┘       └┘└─┘└┘     
typ    └───┘      └┘└─┘└┘   
doc    └───┘       └┘└─┘└┘     
txt    └───┘         └─┘        
par    └───┘         └─┘        
pid    └───┘         └─┘        
st   ────────────────────────────────────────┘└─
691    { assume e he,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ──────────────┘└─
692      let ε := min (e - f x) 1,
id                └─┘      
src      └───────┘└─┘     └─┘
typ      └───────┘└─┘  └─┘
doc      └───────┘        └─┘
txt      └───────┘        └─┘
par      └───────┘        └─┘
pid      └───┘└─┘        └┘
st   ───────────────────────────┘└─
693      have : ε < ⊤ := lt_of_le_of_lt (min_le_right _ _) (by simp [lt_top_iff_ne_top]),
id                      └────────────┘  └──────────┘                └───────────────┘
src      └─────┘   └──┘└────────────┘ └──────────┘└────┘   └────┘└───────────────┘
typ      └─────┘  └──┘└────────────┘ └──────────┘└────┘   └────┘└───────────────┘
doc      └─────┘   └──┘                           └────┘   └────┘                 
txt      └─────┘   └──┘                           └────┘   └────┘                 
par      └─────┘   └──┘                           └────┘   └────┘                 
pid      └───┘└┘   └──┘                           └────┘   └─────┘                 └┘
st   ────────────────────────────────────────────────────────┘└───────────────────────┘└─
694      have : 0 < ε := by simp [ε, he, ennreal.zero_lt_one],
id                                 └┘  └─────────────────┘
src      └───────┘  └──┘  └────┘ └┘  └┘└─────────────────┘
typ      └───────┘ └──┘  └────┘└┘└┘└┘└─────────────────┘
doc      └───────┘  └──┘  └────┘ └┘  └┘                   
txt      └───────┘  └──┘  └────┘ └┘  └┘                   
par      └───────┘  └──┘  └────┘ └┘  └┘                   
pid      └───┘└──┘  └──┘  └─────┘ └┘  └┘                   
st   ─────────────────────┘└────────────────────────────────┘└─
695      have : 0 < C⁻¹ * (ε/2) := bot_lt_iff_ne_bot.2 (by simp [hC, (ne_of_lt this).symm, ennreal.mul_eq_zero]),
id                               └───────────────┘             └┘   └──────┘ └──┘        └─────────────────┘
src      └───────┘        └────┘└───────────────┘└─┘   └────┘  └┘ └──────┘    └──────┘└─────────────────┘
typ      └───────┘      └────┘└───────────────┘└─┘   └────┘└┘└┘ └──────┘└──┘└──────┘└─────────────────┘
doc      └───────┘        └────┘                 └─┘   └────┘  └┘             └──────┘                   
txt      └───────┘        └────┘                 └─┘   └────┘  └┘             └──────┘                   
par      └───────┘        └────┘                 └─┘   └────┘  └┘             └──────┘                   
pid      └───┘└──┘        └┘└──┘                 └─┘   └─────┘  └┘             └──────┘                   └┘
st   ────────────────────────────────────────────────────┘└───────────────────────────────────────────────────┘└─
696      have I : C * (C⁻¹ * (ε/2)) < ε,
id                                   
src      └───────┘          └──┘ 
typ      └───────┘         └──┘ 
doc      └───────┘          └──┘ 
txt      └───────┘          └──┘ 
par      └───────┘          └──┘ 
pid      └────┘└─┘          └──┘ 
st   ─────────────────────────────────┘└─
697      { by_cases C_zero : C = 0,
id                           
src        └───────┘      └─┘  └┘
typ        └───────┘      └─┘ └┘
doc        └───────┘      └─┘  └┘
txt        └───────┘      └─┘  └┘
par        └───────┘      └─┘  └┘
pid                      └─┘  
st   ─────┘└─────────────────────┘└─
698        simp [C_zero, ‹0 < ε›],
id               └────┘       
src        └────┘      └┘ └┘   
typ        └────┘└────┘└┘ └┘  
doc        └────┘      └┘ └┘   
txt        └────┘      └┘ └┘   
par        └────┘      └┘ └┘   
pid                  └┘ └┘   
st   ───────────────────────────┘└─
699        calc C * (C⁻¹ * (ε/2)) = (C * C⁻¹) * (ε/2) : by simp [mul_assoc]
id         └──┘                                                 └───────┘
src        └──┘                                            └────┘└───────┘└─
typ        └──┘                                           └────┘└───────┘└─
doc        └──┘                                            └────┘         └─
txt                                                        └────┘         └─
par                                                        └────┘         └─
pid                                                                     
st   ────────────────────────────────────────────────────┘└─────────────────
700          ... = ε/2 : by simp [ennreal.mul_inv_cancel C_zero hC]
id                                └────────────────────┘ └────┘ └┘
src  ───────┘               └────┘└────────────────────┘        └─
typ  ───────┘               └────┘└────────────────────┘└────┘└┘└─
doc  ───────┘               └────┘                              └─
txt  ───────┘               └────┘                              └─
par  ───────┘               └────┘                              └─
pid  ───────┘                                                 
st   ───────┘└────────────┘└────────────────────────────────────────
701          ... < ε : ennreal.half_lt_self (bot_lt_iff_ne_bot.1 ‹0 < ε›) (lt_top_iff_ne_top.1 ‹ε < ⊤›) },
id                     └──────────────────┘  └───────────────┘             └───────────────┘    
src  ───────┘          └──────────────────┘  └───────────────┘             └───────────────┘
typ  ───────┘          └──────────────────┘  └───────────────┘             └───────────────┘    
doc  ───────┘
txt  ───────┘
par  ───────┘
pid  ───────┘
st   ───────┘└────────────────────────────────────────────────────────────────────────────────────────┘└─┘
702      have : ball x (C⁻¹ * (ε/2)) ⊆ {y : α | f y < e},
id              └──┘                            
src      └─────┘└──┘         └──┘ └──┘ └─┘    
typ      └─────┘└──┘      └──┘ └──┘└─┘  
doc      └─────┘└──┘         └──┘  └──┘ └─┘    
txt      └─────┘             └──┘  └──┘ └─┘    
par      └─────┘             └──┘  └──┘ └─┘    
pid      └───┘└┘             └──┘  └──┘ └─┘    
st   ──────────────────────────────────────────────────┘└─
703      { rintros y hy,
src        └──────────┘
typ        └──────────┘
doc        └──────────┘
txt        └──────────┘
par        └──────────┘
pid               └───┘
st   ─────┘└──────────┘└─
704        have htop : f x ≠ ⊤ := ne_top_of_lt he,
id                             └──────────┘ └┘
src        └──────────┘   └──┘└──────────┘
typ        └──────────┘ └──┘└──────────┘└┘
doc        └──────────┘    └──┘            
txt        └──────────┘    └──┘            
par        └──────────┘    └──┘            
pid        └───────┘└─┘    └──┘            
st   ───────────────────────────────────────────┘└─
705        show f y < e, from calc
id                  
src        └───┘      └───┘    
typ        └───┘   └───┘    
doc        └───┘      └───┘    
txt        └───┘      └───┘    
par        └───┘      └───┘    
pid        └───┘      └───┘    
st   ─────────────────┘└───────────
706          f y ≤ f x + C * edist y x : h y x
id                         └───┘         
src  ───────┘        └───┘  └─┘   
typ  ───────┘      └───┘  └─┘
doc  ───────┘               └─┘   
txt  ───────┘               └─┘   
par  ───────┘               └─┘   
pid  ───────┘               └─┘   
st   ──────────────────────────────────────────
707          ... ≤ f x + C * (C⁻¹ * (ε/2)) :
id                                   
src  ───────────┘              └─────
typ  ───────────┘             └─────
doc  ───────────┘              └─────
txt  ───────────┘              └─────
par  ───────────┘              └─────
pid  ───────────┘              └─────
st   ────────────────────────────────────────
708              add_le_add_left' $ canonically_ordered_semiring.mul_le_mul (le_refl _) (le_of_lt hy)
id                                  └─────────────────────────────────────┘  └─────┘     └──────┘ └┘
src  ───────────┘                 └─────────────────────────────────────┘ └─────┘└──┘ └──────┘  └─
typ  ───────────┘                 └─────────────────────────────────────┘ └─────┘└──┘ └──────┘└┘└─
doc  ───────────┘                                                                └──┘           └─
txt  ───────────┘                                                                └──┘           └─
par  ───────────┘                                                                └──┘           └─
pid  ───────────┘                                                                └──┘           └─
st   ─────────────────────────────────────────────────────────────────────────────────────────────────
709          ... < f x + ε : (ennreal.add_lt_add_iff_left (lt_top_iff_ne_top.2 htop)).2 I
id                            └─────────────────────────┘  └───────────────┘   └──┘     
src  ───────────┘     └─┘ └─────────────────────────┘ └───────────────┘└─┘    └───┘ 
typ  ───────────┘     └─┘ └─────────────────────────┘ └───────────────┘└─┘└──┘└───┘
doc  ───────────┘     └─┘                                              └─┘    └───┘ 
txt  ───────────┘     └─┘                                              └─┘    └───┘ 
par  ───────────┘     └─┘                                              └─┘    └───┘ 
pid  ───────────┘     └─┘                                              └─┘    └───┘ 
st   ─────────────────────────────────────────────────────────────────────────────────────
710          ... ≤ f x + (e - f x) : add_le_add_left' (min_le_left _ _)
id                                   └──────────────┘  └─────────┘
src  ───────────┘         └──┘└──────────────┘ └─────────┘└─────
typ  ───────────┘         └──┘└──────────────┘ └─────────┘└─────
doc  ───────────┘         └──┘                            └─────
txt  ───────────┘         └──┘                            └─────
par  ───────────┘         └──┘                            └─────
pid  ───────────┘         └──┘                            └─────
st   ───────────────────────────────────────────────────────────────────
711          ... = e : by simp [le_of_lt he] },
id                             └──────┘ └┘
src  ───────────┘  └─┘  └────┘└──────┘  └┘
typ  ───────────┘ └─┘  └────┘└──────┘└┘└┘
doc  ───────────┘  └─┘  └────┘          └┘
txt  ───────────┘  └─┘  └────┘          └┘
par  ───────────┘  └─┘  └────┘          └┘
pid  ───────────┘  └─┘  └─────┘          └┘
st   ───────────────────┘└──────────────────┘└┘
712      apply filter.mem_sets_of_superset (ball_mem_nhds _ (‹0 < C⁻¹ * (ε/2)›)) this },
id             └─────────────────────────┘  └───────────┘                      └──┘
src      └────┘└─────────────────────────┘ └───────────┘└─┘  └┘        └┘ └─┘    
typ      └────┘└─────────────────────────┘ └───────────┘└─┘  └┘      └┘ └─┘└──┘
doc      └────┘                                         └─┘  └┘        └┘ └─┘    
txt      └────┘                                         └─┘  └┘        └┘ └─┘    
par      └────┘                                         └─┘  └┘        └┘ └─┘    
pid                                                    └─┘  └┘        └┘ └─┘    
st   ────────────────────────────────────────────────────────────────────────────────┘└──
713  end
st   ──┘
714  
715  theorem continuous_edist' : continuous (λp:α×α, edist p.1 p.2) :=
id                               └────────┘       └───┘   
src                              └────────┘         └───┘     
typ                              └────────┘       └───┘   
doc                              └────────┘
716  begin
st   └─────
717    apply continuous_of_le_add_edist 2 (by simp),
id           └────────────────────────┘
src    └────┘└────────────────────────┘└─┘   └──┘
typ    └────┘└────────────────────────┘└─┘   └──┘
doc    └────┘                          └─┘   └──┘
txt    └────┘                          └─┘   └──┘
par    └────┘                          └─┘   └──┘
pid                                   └─┘   └────┘
st   ───────────────────────────────────────┘└───┘└─
718    rintros ⟨x, y⟩ ⟨x', y'⟩,
src    └─────────────────────┘
typ    └─────────────────────┘
doc    └─────────────────────┘
txt    └─────────────────────┘
par    └─────────────────────┘
pid           └──────────────┘
st   ────────────────────────┘└─
719    calc edist x y ≤ edist x x' + edist x' y' + edist y' y : edist_triangle4 _ _ _ _
id     └──┘                               └┘      └───┘ └┘    └─────────────┘
src    └──┘                                        └───┘        └─────────────┘
typ    └──┘                               └┘      └───┘ └┘    └─────────────┘
doc    └──┘
st   ───────────────────────────────────────────────────────────────────────────────────
720      ... = edist x' y' + (edist x x' + edist y y') : by simp [add_comm, edist_comm]
id                                                                └──────┘  └────────┘
src                                                         └────┘└──────┘└┘└────────┘└─
typ                                                         └────┘└──────┘└┘└────────┘└─
doc                                                         └────┘        └┘          └─
txt                                                         └────┘        └┘          └─
par                                                         └────┘        └┘          └─
pid                                                                     └┘          
st   ─────────────────────────────────────────────────────┘└────────────────────────────
721      ... ≤ edist x' y' + (edist (x, y) (x', y') + edist (x, y) (x', y')) :
id                                 
src  ───┘                          
typ  ───┘                          
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─────────────────────────────────────────────────────────────────────
722        add_le_add_left' (add_le_add' (by simp [edist, le_refl]) (by simp [edist, le_refl]))
id         └──────────────┘  └─────────┘                  └─────┘                    └─────┘
src        └──────────────┘  └─────────┘     └────┘     └┘└─────┘      └────┘     └┘└─────┘
typ        └──────────────┘  └─────────┘     └────┘     └┘└─────┘      └────┘     └┘└─────┘
doc                                          └────┘     └┘             └────┘     └┘       
txt                                          └────┘     └┘             └────┘     └┘       
par                                          └────┘     └┘             └────┘     └┘       
pid                                                   └┘                      └┘       
st   ──────────────────────────────────────┘└────────────────────┘└───┘└────────────────────┘└──
723      ... = edist x' y' + 2 * edist (x, y) (x', y') : by rw [← mul_two, mul_comm]
id                                                               └─────┘  └──────┘
src                                                        └────┘└─────┘└┘└──────┘└┘
typ                                                        └────┘└─────┘└┘└──────┘└┘
doc                                                         └────┘       └┘        └┘
txt                                                         └────┘       └┘        └┘
par                                                         └────┘       └┘        └┘
pid                                                           └──┘       └┘        
st   ─────────────────────────────────────────────────────┘└────────────┘└────────┘
724  end
st   └─┘
725  
726  theorem continuous_edist [topological_space β] {f g : β → α}
id                             └───────────────┘             
src                            └───────────────┘
typ                            └───────────────┘             
doc                            └───────────────┘
727    (hf : continuous f) (hg : continuous g) : continuous (λb, edist (f b) (g b)) :=
id           └────────┘         └────────┘     └────────┘     └───┘       
src          └────────┘          └────────┘      └────────┘      └───┘
typ          └────────┘         └────────┘     └────────┘     └───┘       
doc          └────────┘          └────────┘      └────────┘
728  continuous_edist'.comp (hf.prod_mk hg)
id   └───────────────┘└───┘  └┘└──────┘ └┘
src  └───────────────┘└───┘    └──────┘
typ  └───────────────┘└───┘  └┘└──────┘ └┘
729  
730  theorem tendsto_edist {f g : β → α} {x : filter β} {a b : α}
id                                          └────┘          
src                                           └────┘
typ                                         └────┘          
731    (hf : tendsto f x (𝓝 a)) (hg : tendsto g x (𝓝 b)) :
id           └─────┘              └─────┘     
src          └─────┘                 └─────┘      
typ          └─────┘              └─────┘     
doc          └─────┘                 └─────┘      
732    tendsto (λx, edist (f x) (g x)) x (𝓝 (edist a b)) :=
id     └─────┘     └───┘              └───┘  
src    └─────┘      └───┘                   └───┘
typ    └─────┘     └───┘              └───┘  
doc    └─────┘                            
733  have tendsto (λp:α×α, edist p.1 p.2) (𝓝 (a, b)) (𝓝 (edist a b)),
id        └─────┘       └───┘                └───┘  
src       └─────┘         └───┘                    └───┘
typ       └─────┘       └───┘                └───┘  
doc       └─────┘                                    
734    from continuous_iff_continuous_at.mp continuous_edist' (a, b),
id          └──────────────────────────┘└─┘ └───────────────┘   
src         └──────────────────────────┘└─┘ └───────────────┘ 
typ         └──────────────────────────┘└─┘ └───────────────┘   
735  tendsto.comp (by rw [nhds_prod_eq] at this; exact this) (hf.prod_mk hg)
id   └──────────┘         └──────────┘                 └──┘   └┘└──────┘ └┘
src  └──────────┘     └──┘└──────────┘└───────┘  └────┘         └──────┘
typ  └──────────┘     └──┘└──────────┘└───────┘  └────┘└──┘   └┘└──────┘ └┘
doc                   └──┘            └───────┘  └────┘
txt                   └──┘            └───────┘  └────┘
par                   └──┘            └───────┘  └────┘
pid                     └┘            └──────┘       
st                   └───────────────┘└──────────────────┘
736  
737  lemma cauchy_seq_of_edist_le_of_tsum_ne_top {f : ℕ → α} (d : ℕ → ennreal)
id                                                                 └─────┘
src                                                                 └─────┘
typ                                                                └─────┘
doc                                                                   └─────┘
738    (hf : ∀ n, edist (f n) (f n.succ) ≤ d n) (hd : tsum d ≠ ∞) :
id               └───┘       └───┘            └──┘   
src               └───┘           └───┘              └──┘    
typ              └───┘       └───┘            └──┘   
doc                                                   └──┘     
739    cauchy_seq f :=
id     └────────┘ 
src    └────────┘
typ    └────────┘ 
doc    └────────┘
740  begin
st   └─────
741    lift d to (ℕ → nnreal) using (λ i, ennreal.ne_top_of_tsum_ne_top hd i),
id                   └────┘              └───────────────────────────┘ └┘
src    └───┘ └──┘   └────┘└──────┘  └──┘└───────────────────────────┘   
typ    └───┘└──┘   └────┘└──────┘  └──┘└───────────────────────────┘└┘ 
doc    └───┘ └──┘   └────┘└──────┘  └──┘                                
txt    └───┘ └──┘         └──────┘  └──┘                                
par    └───┘ └──┘         └──────┘  └──┘                                
pid         └──┘         └─────┘  └──┘                                
st   ───────────────────────────────────────────────────────────────────────┘└─
742    rw ennreal.tsum_coe_ne_top_iff_summable at hd,
id        └──────────────────────────────────┘
src    └─┘└──────────────────────────────────┘└────┘
typ    └─┘└──────────────────────────────────┘└────┘
doc    └─┘                                    └────┘
txt    └─┘                                    └────┘
par    └─┘                                    └────┘
pid                                          └────┘
st   ──────────────────────────────────────────────┘└─
743    exact cauchy_seq_of_edist_le_of_summable d hf hd
id           └────────────────────────────────┘  └┘ └┘
src    └────┘└────────────────────────────────┘     
typ    └────┘└────────────────────────────────┘└┘└┘
doc    └────┘└────────────────────────────────┘     
txt    └────┘                                       
par    └────┘                                       
pid                                                
st   ──────────────────────────────────────────────────┘
744  end
st   └─┘
745  
746  /-- If `edist (f n) (f (n+1))` is bounded above by a function `d : ℕ → ennreal`,
747  then the distance from `f n` to the limit is bounded by `∑_{k=n}^∞ d k`. -/
748  lemma edist_le_tsum_of_edist_le_of_tendsto {f : ℕ → α} (d : ℕ → ennreal)
id                                                                └─────┘
src                                                                └─────┘
typ                                                               └─────┘
doc                                                                  └─────┘
749    (hf : ∀ n, edist (f n) (f n.succ) ≤ d n)
id               └───┘       └───┘    
src               └───┘           └───┘  
typ              └───┘       └───┘    
750    {a : α} (ha : tendsto f at_top (𝓝 a)) (n : ℕ) :
id                  └─────┘  └────┘           
src                  └─────┘   └────┘            
typ                 └─────┘  └────┘           
doc                  └─────┘   └────┘  
751    edist (f n) a ≤ ∑ m, d (n + m) :=
id     └───┘             
src    └───┘                  
typ    └───┘             
doc                      
752  begin
st   └─────
753    refine le_of_tendsto at_top_ne_bot (tendsto_edist tendsto_const_nhds ha)
id            └───────────┘ └───────────┘  └───────────┘ └────────────────┘ └┘
src    └─────┘└───────────┘└───────────┘ └───────────┘└────────────────┘  └─
typ    └─────┘└───────────┘└───────────┘ └───────────┘└────────────────┘└┘└─
doc    └─────┘                                                            └─
txt    └─────┘                                                            └─
par    └─────┘                                                            └─
pid                                                                      └─
st   ───────────────────────────────────────────────────────────────────────────
754      (mem_at_top_sets.2 ⟨n, λ m hnm, _⟩),
id        └─────────────┘    
src  ───┘ └─────────────┘└─┘  └┘ └─────────┘
typ  ───┘ └─────────────┘└─┘ └┘ └─────────┘
doc  ───┘                └─┘  └┘ └─────────┘
txt  ───┘                └─┘  └┘ └─────────┘
par  ───┘                └─┘  └┘ └─────────┘
pid  ───┘                └─┘  └┘ └─────────┘
st   ──────────────────────────────────────┘└─
755    refine le_trans (edist_le_Ico_sum_of_edist_le hnm (λ k _ _, hf k)) _,
id            └──────┘  └──────────────────────────┘ └─┘           └┘
src    └─────┘└──────┘ └──────────────────────────┘     └──────┘   └──┘
typ    └─────┘└──────┘ └──────────────────────────┘└─┘  └──────┘└┘ └──┘
doc    └─────┘         └──────────────────────────┘     └──────┘   └──┘
txt    └─────┘                                          └──────┘   └──┘
par    └─────┘                                          └──────┘   └──┘
pid                                                    └──────┘   └──┘
st   ─────────────────────────────────────────────────────────────────────┘└─
756    rw [finset.sum_Ico_eq_sum_range],
id         └─────────────────────────┘
src    └──┘└─────────────────────────┘
typ    └──┘└─────────────────────────┘
doc    └──┘                           
txt    └──┘                           
par    └──┘                           
pid      └┘                           
st   ────────────────────────────────┘└──
757    exact sum_le_tsum _ (λ _ _, zero_le _) ennreal.summable
id           └─────────┘           └─────┘    └──────────────┘
src    └────┘└─────────┘└─┘  └────┘└─────┘└──┘└──────────────┘
typ    └────┘└─────────┘└─┘  └────┘└─────┘└──┘└──────────────┘
doc    └────┘           └─┘  └────┘       └──┘                
txt    └────┘           └─┘  └────┘       └──┘                
par    └────┘           └─┘  └────┘       └──┘                
pid                    └─┘  └────┘       └──┘                
st   ─────────────────────────────────────────────────────────┘
758  end
st   └─┘
759  
760  /-- If `edist (f n) (f (n+1))` is bounded above by a function `d : ℕ → ennreal`,
761  then the distance from `f 0` to the limit is bounded by `∑_{k=0}^∞ d k`. -/
762  lemma edist_le_tsum_of_edist_le_of_tendsto₀ {f : ℕ → α} (d : ℕ → ennreal)
id                                                                 └─────┘
src                                                                 └─────┘
typ                                                                └─────┘
doc                                                                   └─────┘
763    (hf : ∀ n, edist (f n) (f n.succ) ≤ d n)
id               └───┘       └───┘    
src               └───┘           └───┘  
typ              └───┘       └───┘    
764    {a : α} (ha : tendsto f at_top (𝓝 a)) :
id                  └─────┘  └────┘   
src                  └─────┘   └────┘  
typ                 └─────┘  └────┘   
doc                  └─────┘   └────┘  
765    edist (f 0) a ≤ ∑ m, d m :=
id     └───┘           
src    └───┘            
typ    └───┘           
doc                      
766  by simpa using edist_le_tsum_of_edist_le_of_tendsto d hf ha 0
id                  └──────────────────────────────────┘  └┘ └┘
src     └──────────┘└──────────────────────────────────┘     └──
typ     └──────────┘└──────────────────────────────────┘└┘└┘└──
doc     └──────────┘└──────────────────────────────────┘     └──
txt     └──────────┘                                         └──
par     └──────────┘                                         └──
pid          └────┘                                         └─
st     └───────────────────────────────────────────────────────────
767  
src  
typ  
doc  
txt  
par  
pid  
st   
768  end --section